diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | Makefile.build | 18 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | configure.ml | 5 |
4 files changed, 9 insertions, 17 deletions
diff --git a/.gitignore b/.gitignore index 8f0a9a409..5b4ffa77b 100644 --- a/.gitignore +++ b/.gitignore @@ -139,7 +139,6 @@ tactics/extratactics.ml tactics/extraargs.ml toplevel/whelp.ml ide/coqide_main.ml -ide/coqide_main_opt.ml # other auto-generated files diff --git a/Makefile.build b/Makefile.build index 075638a23..d45a0cbd3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -317,9 +317,8 @@ coqide-files: $(IDEFILES) ifeq ($(HASCOQIDE),opt) $(COQIDE): $(LINKIDEOPT) | $(COQTOPEXE) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa \ - lablgtk.cmxa lablgtksourceview2.cmxa $(IDEOPTFLAGS) \ - str.cmxa $(LINKIDEOPT) + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa lablgtk.cmxa \ + lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $(LINKIDEOPT) $(STRIP) $@ else $(COQIDE): $(COQIDEBYTE) @@ -329,12 +328,11 @@ endif $(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma lablgtk.cma \ - lablgtksourceview2.cma str.cma $(LINKIDE) + lablgtksourceview2.cma str.cma $(IDEFLAGS) $(LINKIDE) # install targets -.PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt -.PHONY: install-ide-files install-ide-info install-im install-ide-devfiles +.PHONY: install-coqide install-ide-bin install-ide-files install-ide-info install-ide-devfiles ifeq ($(HASCOQIDE),no) install-coqide: @@ -358,7 +356,7 @@ install-ide-files: $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) - if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi + if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi install-ide-info: $(MKDIR) $(FULLDOCDIR) @@ -750,14 +748,10 @@ grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $^ -linkall -a -o $@ -ide/coqide_main.ml: ide/coqide_main.ml4 +ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ -ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@ - # pretty printing of the revision number when compiling a checked out # source tree .PHONY: revision diff --git a/Makefile.common b/Makefile.common index 06d97567b..966829d5a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -214,7 +214,7 @@ IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo l IDECMA:=ide/ide.cma LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml +LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml # modules known by the toplevel of Coq diff --git a/configure.ml b/configure.ml index 79087a405..5488904a1 100644 --- a/configure.ml +++ b/configure.ml @@ -741,7 +741,7 @@ let coqide_flags () = let osxdir = tryrun "ocamlfind" ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; - idearchflags := "lablgtkosx.cmxa"; + idearchflags := "lablgtkosx.cma"; idearchdef := "QUARTZ" end | "opt", "win32" -> @@ -1113,9 +1113,8 @@ let write_makefile f = pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes; pr "# CoqIde (no/byte/opt)\n"; pr "HASCOQIDE=%s\n" coqide; - pr "IDEOPTFLAGS=%s\n" !idearchflags; + pr "IDEFLAGS=%s\n" !idearchflags; pr "IDEOPTDEPS=%s\n" !idearchfile; - pr "IDEOPTINT=%s\n\n" !idearchdef; pr "IDEINT=%s\n\n" !idearchdef; pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; |