diff options
| author | letouzey | 2011-03-23 17:18:57 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-23 17:18:57 +0000 |
| commit | e84e0f9e4eb6263e870deb1e00929170bc0301ea (patch) | |
| tree | 7a792a8f40c5328c0bd385cec13cb4a65a6b8a3d /Makefile.common | |
| parent | 461798eeecfd2a59159fb9666874d8ea14209624 (diff) | |
Ide: stronger separation from coqtop
Former module Ide_blob is now divided in Ide_intf (linked both
by coqtop and coqide) and Ide_slave (now only in coqtop).
Ide_intf has almost no dependencies, we can now compile coqide
with only coq_config.cm* and lib.cm(x)a
TODO:
- Devise a better way to display whether coqide is byte or opt
in the about message (instead of Mltop.is_native, I display
now the executable name, which hopefully contains opt or byte)
- Check the late error handling in ide/coq.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index fa76dac60b..c51ca4011a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -217,10 +217,15 @@ INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS)) LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) +LIBCMA:=lib/lib.cma IDECMA:=ide/ide.cma +IDEINTF:=toplevel/ide_intf.cmo -LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTDEPS) $(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml +IDELIBS:=$(CONFIG) $(LIBCMA) $(IDEINTF) $(IDECMA) +IDELIBSOPT:=$(subst .cmo,.cmx,$(IDELIBS:.cma=.cmxa)) + +LINKIDE:=$(IDELIBS) ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTDEPS) $(IDELIBSOPT) ide/coqide_main_opt.ml # modules known by the toplevel of Coq |