aboutsummaryrefslogtreecommitdiff
path: root/Makefile.install
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.install')
-rw-r--r--Makefile.install5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.install b/Makefile.install
index 4977bb38e1..0dd4c1bc24 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -162,8 +162,9 @@ install-latex:
$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
# -$(UPDATETEX)
-install-meta: META.coq
- $(INSTALLLIB) META.coq $(FULLCOQLIB)/META
+install-meta: META.coq-core
+ $(INSTALLLIB) META.coq-core $(FULLCOQLIB)/META
+ cd $(FULLCOQLIB)/.. && rm -f coq-core && ln -s coq coq-core
# For emacs:
# Local Variables: