From 2ccec00285b3bf67d230eedda120cd72c328cfbb Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 23 May 2018 20:22:56 -0700
Subject: Don't try to install native compiled files if native-compile is not
 set

---
 Makefile.install | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.install')

diff --git a/Makefile.install b/Makefile.install
index 0764b61fc7..984cfc05cc 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -82,7 +82,7 @@ endif
 
 install-tools:
 	$(MKDIR) $(FULLBINDIR)
-	# recopie des fichiers de style pour coqide
+	# copy style files for coqide
 	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
 	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
 	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
-- 
cgit v1.2.3