aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/merlin1/run.sh
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile/merlin1/run.sh')
-rwxr-xr-xtest-suite/coq-makefile/merlin1/run.sh4
1 files changed, 1 insertions, 3 deletions
diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh
index 752c0c2cea..1f262a9390 100755
--- a/test-suite/coq-makefile/merlin1/run.sh
+++ b/test-suite/coq-makefile/merlin1/run.sh
@@ -1,11 +1,9 @@
#!/usr/bin/env bash
-#set -x
-set -e
-
. ../template/init.sh
coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
make .merlin
cat > desired <<EOT
B src