diff options
| author | coq | 2004-02-23 16:50:09 +0000 |
|---|---|---|
| committer | coq | 2004-02-23 16:50:09 +0000 |
| commit | 553e548b8c7efb7aa69f1f6a50a11c4bcd97ab64 (patch) | |
| tree | aea7c1a20bff1a65f2d147319365207da10acb76 /dev | |
| parent | 6032ae1dfaf2f9313aad8277b44df1d9d0cc8d91 (diff) | |
Generating of annotations added to Makefile.dir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/Makefile.dir | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/dev/Makefile.dir b/dev/Makefile.dir index 80fe5834c6..54f7bfe9ff 100644 --- a/dev/Makefile.dir +++ b/dev/Makefile.dir @@ -107,6 +107,13 @@ pretty: depend.ps echo Generated interface file $@ ; \ mv -f $$cmo.tmp $$cmo) +%.annot: FORCE + @(cmo=`basename $@ .annot`.cmo ; \ + mv -f $$cmo $$cmo.tmp ; \ + $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \ + echo Generated annotation file $@ ; \ + mv -f $$cmo.tmp $$cmo) + FORCE: clean:: @@ -114,11 +121,10 @@ clean:: # this is not perfect but mostly WORKS! It just calls the main makefile -%.cmi: *.mli +%.cmi: FORCE $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ -SOURCES=$(wildcard *.mli) $(wildcard *.ml) $(wildcard *.ml4) -%.cmo: $(SOURCES) +%.cmo: FORCE $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@ coqtop: |