diff options
| author | Gaëtan Gilbert | 2018-11-26 15:04:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-06 15:13:49 +0100 |
| commit | e3a2a5d4fc3ad29462f2e4548c32ac00b4fbd05f (patch) | |
| tree | 4470538f3e0862f4b503882416162aafb2e47879 /Makefile.install | |
| parent | f3a7d021e6b347c2c0edf3c07f3206f22dcdf39a (diff) | |
Rename generated directory gramlib__pack -> gramlib/.pack
It's a bit cleaner this way, especially wrt the number of toplevel directories.
Also fix warning about undefined GRAMMARCMA while we're at it.
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 |