diff --git a/doc/fixing_tests.md b/doc/fixing_tests.md
index 84f5fcbb4e..ce67aa68ab 100644
--- a/doc/fixing_tests.md
+++ b/doc/fixing_tests.md
@@ -30,6 +30,8 @@ When the `yes` option is provided, `meld` is automatically invoked
 whenever there is discrepancy between the produced and expected
 outputs. `meld` can also be used to repair the problems.
 
+In Emacs, we can also execute `M-x lean-diff-test-file` to check/diff the file of the current buffer.
+
 Here is the list of directories where produced output is compared with
 the expected output (stored in a `*.expected.out` file).
 
@@ -37,5 +39,5 @@ the expected output (stored in a `*.expected.out` file).
 - [`tests/lean/interactive`](../tests/lean/interactive)
 
 Remark: in the directory `tests/lean/interactive`, the input test files have extension `.input`.
-They simulate commands sent from Emacs to Lean.
-The `.lean` files in this directory are used to simulate files opened by the user.
\ No newline at end of file
+They simulate commands sent from editors to Lean.
+The `.lean` files in this directory are used to simulate files opened by the user.
diff --git a/src/emacs/lean-dev.el b/src/emacs/lean-dev.el
new file mode 100644
index 0000000000..c669274ff6
--- /dev/null
+++ b/src/emacs/lean-dev.el
@@ -0,0 +1,16 @@
+;;  -*- lexical-binding: t -*-
+;;
+;; Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Sebastian Ullrich
+;;
+
+(defun lean-diff-test-file ()
+  "Use interactive ./test_input.sh on file of current buffer"
+  (interactive)
+  (message (shell-command-to-string (format "./test_single.sh \"%s\" \"%s\" yes"
+                                            (lean-get-executable "lean")
+                                            (buffer-name)))))
+
+(provide 'lean-dev)
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 2aad5fe366..adbdd8e4bc 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -33,6 +33,7 @@
 (require 'lean-type)
 (require 'lean-message-boxes)
 (require 'lean-right-click)
+(require 'lean-dev)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"