diff options
| author | Emilio Jesus Gallego Arias | 2018-12-10 14:08:56 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-10 14:08:56 +0100 |
| commit | 3f014b0c883cd71cf751b0ccc297edb38e46ae47 (patch) | |
| tree | cacc5fe6e908f7ba7ef1c99f0235da1f2876c7fa /Makefile.install | |
| parent | 01f4470c330ce52b03046d5b98cd5af3ac87272e (diff) | |
| parent | e3a2a5d4fc3ad29462f2e4548c32ac00b4fbd05f (diff) | |
Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.pack
Diffstat (limited to 'Makefile.install')
| -rw-r--r-- | Makefile.install | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/Makefile.install b/Makefile.install index 8233807e03..b6e2ec2aeb 100644 --- a/Makefile.install +++ b/Makefile.install @@ -92,17 +92,20 @@ install-tools: INSTALLCMI = $(sort \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ + $(filter %.cmi, $(GRAMMLFILES:.mli=.cmi)) gramlib/.pack/gramlib.cmi \ $(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \ - $(PLUGINS:.cmo=.cmi) gramlib__pack/gramlib.cmi + $(PLUGINS:.cmo=.cmi) INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% \ configure.cmx toplevel/coqtop_byte_bin.cmx plugins/extraction/big.cmx, \ - $(MLFILES:.ml=.cmx))) + $(filter %.cmx, $(GRAMMLFILES:.ml=.cmx)) $(MLFILES:.ml=.cmx))) + +foo: + @echo $(INSTALLCMX) install-devfiles: $(MKDIR) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) # Regular CMI files $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMX) # To avoid warning 58 "-opaque" $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSCMO:.cmo=.cmx) # For static linking of plugins |