From 9973cd2ca529076388710e90f2c46180581397cf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 24 Oct 2014 18:37:10 +0200
Subject: Install index_urls.txt in a location where coqide might actually find
 it.

---
 Makefile.doc | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 6dc27e138..59382b9de 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -328,9 +328,8 @@ install-doc-printable:
 	$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps
 
 install-doc-index-urls:
-	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
-	$(INSTALLLIB) $(INDEXURLS) \
-		$(FULLDOCDIR)/html/refman 
+	$(MKDIR) $(FULLDATADIR)
+	$(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR)
 
 # For emacs:
 # Local Variables:
-- 
cgit v1.2.3