diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:56:37 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:56:37 +0100 |
| commit | fcdddca6124eec4d34e1f57a39aadbd2b082ffcf (patch) | |
| tree | 223cd97353c601729e496fabde16ed06b4cb19de /Makefile.build | |
| parent | b6e05e2944c2a7976c4ac1f51694b175f52dbaf8 (diff) | |
| parent | ffb7ada29308398746decc538c81b608ca57f88c (diff) | |
Merge PR #6305: Build with windows line endings
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 3411e062e..cbc1cbaab 100644 --- a/Makefile.build +++ b/Makefile.build @@ -307,7 +307,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 |