aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-10-29 14:00:58 +0100
committerGaëtan Gilbert2018-11-02 13:48:39 +0100
commite06875ccc11c52b9b9526858c18358a9c4588099 (patch)
tree10ad88829b056036fbc1aad563a7075f345cb594 /dev/tools
parent00a8604d89f47c903fc5283eebdda67c87468699 (diff)
Remove ml4 from Coq's make build system
Diffstat (limited to 'dev/tools')
-rwxr-xr-xdev/tools/change-header2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header
index 61cc866602..687c02f4f1 100755
--- a/dev/tools/change-header
+++ b/dev/tools/change-header
@@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)'
modified=0
kept=0
-for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
+for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
headline=`head -n 1 $i`
if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then
# Has emacs header