aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ocamldebug-v7.template
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ocamldebug-v7.template')
-rw-r--r--dev/ocamldebug-v7.template2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ocamldebug-v7.template b/dev/ocamldebug-v7.template
index a29c6cb0a..68cd59842 100644
--- a/dev/ocamldebug-v7.template
+++ b/dev/ocamldebug-v7.template
@@ -16,7 +16,7 @@ for op in $*
coq-debug-programs.out)
coqdebug="yes"
args="-is programs.coq";;
- coq*) coqdebug="yes";;
+ *coq*) coqdebug="yes";;
esac
done