aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorThéo Zimmermann2019-06-06 11:22:03 +0200
committerThéo Zimmermann2019-06-17 18:04:55 +0200
commit0d5420d3b821a983c5bbdddd254dee4465dc83c7 (patch)
treea964e00dbccd4e680787c30617919289a57d45d2 /dev
parent7e47fea5ce050c8129ba2d6f94e93fbc29763a3b (diff)
Update change-header script to support updating more than just files with ml-style headers.
Diffstat (limited to 'dev')
-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 687c02f4f1..472a075dbd 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 \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
+for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do
headline=`head -n 1 $i`
if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then
# Has emacs header