diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 17:03:18 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-13 17:03:18 +0000 |
| commit | 96641dc219a888965b49abec3b7a34a73c416ba6 (patch) | |
| tree | 0e9ad9910ce7cc761cddd26203230cd2710552ea /dev | |
| parent | 469e9f572f2b7ded2b15c3d98f92969df3140208 (diff) | |
AutoRewrite substitutive...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2965 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/Makefile.dir | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/dev/Makefile.dir b/dev/Makefile.dir index df205c1f6..163f848ad 100644 --- a/dev/Makefile.dir +++ b/dev/Makefile.dir @@ -26,9 +26,12 @@ dir: # make all cmo's in this directory. Useful in case the main Makefile is not # up-to-date all: - @(for i in *.ml{,4}; do \ - echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \ - done \ + @( ( for i in *.ml; do \ + echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \ + done; \ + for i in *.ml4; do \ + echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \ + done ) \ | xargs $(MAKE) -C $(TOPDIR) ) # lists all files that should be compiled in this directory @@ -36,9 +39,12 @@ list: @(for i in *.mli; do \ ls -l `basename $$i .mli`.cmi; \ done) - @(for i in *.ml{,4}; do \ + @(for i in *.ml; do \ ls -l `basename $$i .ml`.cmo; \ done) + @(for i in *.ml4; do \ + ls -l `basename $$i .ml4`.cmo; \ + done) clean:: |