diff options
| author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2023-04-03 12:25:32 (GMT) |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2023-04-03 12:25:32 (GMT) |
| commit | 59ed6a7508cd6552c9b1155983a7a04fcca54092 (patch) | |
| tree | e511f06478eeee806a1dfd724585029dcc4479c6 | |
| parent | 017b3b3c092e8dd5fa0954bef4902623e665e0b5 (diff) | |
| download | coq-v8.5.zip coq-v8.5.tar.gz coq-v8.5.tar.bz2 | |
v8.5: Fix CAMLP4DEPS invocationrefs/pull/17459/headv8.5
The old one worked on bash but not eg debian dash (/bin/sh)
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index b5c933a..057c9ae 100644 --- a/Makefile.build +++ b/Makefile.build @@ -117,7 +117,7 @@ $(if $(findstring $@,$(PRIVATEBINARIES)),\ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef -CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#)) +CAMLP4DEPS=${shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' ${1}} ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) else |