diff options
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: |