summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5198.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/5198.v')
-rw-r--r--test-suite/bugs/closed/5198.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v
index 7254afb4..72722f5f 100644
--- a/test-suite/bugs/closed/5198.v
+++ b/test-suite/bugs/closed/5198.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *)
(* File reduced by coq-bug-finder from original input, then from 286 lines to
27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines,
then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from