aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ErrorInModule.v
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-05-19 10:48:30 +0200
committerPierre-Marie Pédrot2017-05-19 10:48:30 +0200
commit0a67131d9a63e26ea2ea85d9ed51d76d8464295e (patch)
tree980727a88f63908ce1f25f317e43126a0d3d0ad8 /test-suite/output/ErrorInModule.v
parent37e84b83739fec666264904bc06fd32b46b83140 (diff)
parent9f11adda4bff194a3c6a66d573ce7001d4399886 (diff)
Merge branch 'master' into ltac2-hooks
Diffstat (limited to 'test-suite/output/ErrorInModule.v')
-rw-r--r--test-suite/output/ErrorInModule.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
index e69e23276b..b2e3c3e923 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.