diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.checker | 5 |
2 files changed, 4 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 39b793d2b..867c494a1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -302,7 +302,7 @@ kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h -e '/^}/q' $< $(TOTARGET) kernel/copcodes.ml: kernel/byterun/coq_instruct.h - sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \ + tr -d "\r" < $< | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | \ awk -f kernel/make-opcodes $(TOTARGET) %.o: %.c diff --git a/Makefile.checker b/Makefile.checker index 435d8e8f6..f9ed2d957 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -75,8 +75,9 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ - then true; else echo "Error: outdated checker/values.ml"; false; fi + $(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \ + if grep -q "$$v" checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi .PHONY: md5chk |