diff options
| author | lmamane | 2007-08-01 08:28:55 +0000 |
|---|---|---|
| committer | lmamane | 2007-08-01 08:28:55 +0000 |
| commit | 2796108905394fa98588e55e74781b34c0418178 (patch) | |
| tree | 18e7a0bdf3da90cb519b459712011957ff66e40e | |
| parent | e3120308361081906235121b31a0be1397f94fb9 (diff) | |
Build system: BSD compatibility: do not use -printf action of find
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10056 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.common | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Makefile.common b/Makefile.common index 3364edc314..0e61012173 100644 --- a/Makefile.common +++ b/Makefile.common @@ -438,14 +438,14 @@ GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ GENMLIFILES:=$(YACCFILES:.mly=.mli) GENHFILES:=kernel/byterun/coq_jumptbl.h GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) -MLFILES := $(shell find . '(' -name '*.ml' ')' -printf '%P\n' | \ +MLFILES := $(shell find . '(' -name '*.ml' ')' | sed 's|^\./||' | \ while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \ $(GENMLFILES) -MLIFILES := $(shell find . '(' -name '*.mli' ')' -printf '%P\n') \ +MLIFILES := $(shell find . '(' -name '*.mli' ')' | sed 's|^\./||') \ $(GENMLIFILES) -ML4FILES := $(shell find . '(' -name '*.ml4' ')' -printf '%P\n') -VFILES := $(shell find . '(' -name '*.v' ')' -printf '%P\n') -CFILES := $(shell find kernel/byterun -name '*.c' -printf '%p\n') +ML4FILES := $(shell find . '(' -name '*.ml4' ')' | sed 's|^\./||') +VFILES := $(shell find . '(' -name '*.v' ')' | sed 's|^\./||') +CFILES := $(shell find kernel/byterun -name '*.c') ML4FILESML:= $(ML4FILES:.ml4=.ml) |