aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/ErrorInModule.v2
-rw-r--r--test-suite/output/ErrorInSection.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
index e69e23276..b2e3c3e92 100644
--- a/test-suite/output/ErrorInModule.v
+++ b/test-suite/output/ErrorInModule.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
Module M.
Definition foo := nonexistent.
End M.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
index 3036f8f05..505c5ce37 100644
--- a/test-suite/output/ErrorInSection.v
+++ b/test-suite/output/ErrorInSection.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-quick") -*- *)
Section S.
Definition foo := nonexistent.
End S.