diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:34:17 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:34:17 +0200 |
| commit | 75d70664156bf1715b4eb9933a684a344f43467d (patch) | |
| tree | 0f98f6fb7b1d39e8aae86c45ba7b2e36b3a91f53 /Makefile.build | |
| parent | 0c566066f92728d9a848e1f60f52dd09c1a727f2 (diff) | |
| parent | 2def58217686b5083da38778a5ebffb451b1d4d6 (diff) | |
Merge PR #773: [flags] Remove XML output flag.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/Makefile.build b/Makefile.build index 3d4b475dc..92eaf7232 100644 --- a/Makefile.build +++ b/Makefile.build @@ -46,9 +46,6 @@ NO_RECALC_DEPS ?= # Non-empty runs the checker on all produced .vo files: VALIDATE ?= -# Is "-xml" when building XML library: -COQ_XML ?= - # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -189,7 +186,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) +COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) @@ -273,9 +270,6 @@ $(error This Makefile needs GNU Make 3.81 or later (that is a version that suppo endif VO_TOOLS_DEP := $(COQTOPBEST) -ifdef COQ_XML - VO_TOOLS_DEP += $(COQDOC) -endif ifdef VALIDATE VO_TOOLS_DEP += $(CHICKEN) endif @@ -707,9 +701,9 @@ TIMING_EXTRA = endif theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) - $(SHOW)'COQC $(COQ_XML) -noinit $<' + $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) # MExtraction.v generates the ml core file of the micromega tactic. # We check that this generated code is still in sync with the version |