diff options
| author | Gaëtan Gilbert | 2019-11-26 23:01:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-13 13:12:20 +0100 |
| commit | dfb92f3476fff0b329590626790d83a2f9e3e058 (patch) | |
| tree | 2a31c96a4208730fceb08f1ecd8ff041a031d627 /Makefile.install | |
| parent | a07480b5150d23b89a2a9acc09c8e506db9e73da (diff) | |
Split up stdlib install command (too long)
Diffstat (limited to 'Makefile.install')
| -rw-r--r-- | Makefile.install | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/Makefile.install b/Makefile.install index 456c391fd9..dc92062b47 100644 --- a/Makefile.install +++ b/Makefile.install @@ -115,9 +115,18 @@ endif install-merlin: $(INSTALLSH) $(FULLCOQLIB) $(wildcard $(INSTALLCMX:.cmx=.cmt) $(INSTALLCMI:.cmi=.cmti) $(MLIFILES) $(MLFILES) $(MERLINFILES)) +#NB: some files don't produce native files (eg Ltac2 files) as they +#don't have any Coq definitions. Makefile can't predict that so we use || true +#vos build is bugged in -quick mode, see #11195 install-library: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) + $(INSTALLSH) $(FULLCOQLIB) $(ALLVO:.$(VO)=.vo) + $(INSTALLSH) $(FULLCOQLIB) $(ALLVO:.$(VO)=.vos) || true +ifneq ($(NATIVECOMPUTE),) + $(INSTALLSH) $(FULLCOQLIB) $(NATIVEFILES) || true +endif + $(INSTALLSH) $(FULLCOQLIB) $(VFILES) + $(INSTALLSH) $(FULLCOQLIB) $(GLOBFILES) $(MKDIR) $(FULLCOQLIB)/user-contrib $(MKDIR) $(FULLCOQLIB)/kernel/byterun ifndef CUSTOM |