diff options
| author | Maxime Dénès | 2017-09-15 10:37:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-15 10:37:21 +0200 |
| commit | 633b61e7ce82362a5c01724aa54b0e99dcfbb3ab (patch) | |
| tree | f0f3fc2dd964f3f283207d249c93d2e152003616 | |
| parent | 2f22a7f9f7f8369c2edc893e72e131e3b22bb19b (diff) | |
| parent | 3a849429dac4da9acf8538ee4a888ca53b4811cb (diff) | |
Merge PR #1045: Remove unneeded fix for BZ#1715
| -rw-r--r-- | Makefile.install | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.install b/Makefile.install index 85ffc93d51..4800f8f3fa 100644 --- a/Makefile.install +++ b/Makefile.install @@ -87,7 +87,6 @@ install-tools: $(MKDIR) $(FULLBINDIR) # recopie des fichiers de style pour coqide $(MKDIR) $(FULLCOQLIB)/tools/coqdoc - touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) |