aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/output/Emacs_and_diffs.out0
-rw-r--r--test-suite/output/Emacs_and_diffs.v3
2 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/output/Emacs_and_diffs.out b/test-suite/output/Emacs_and_diffs.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/Emacs_and_diffs.out
diff --git a/test-suite/output/Emacs_and_diffs.v b/test-suite/output/Emacs_and_diffs.v
new file mode 100644
index 0000000000..c35fd1a11b
--- /dev/null
+++ b/test-suite/output/Emacs_and_diffs.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-emacs") *)
+Set Diffs "on".
+(* verify this does not produce an error message *)