1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc
index aea5c5628d..3822fc7fb9 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -13,7 +13,7 @@
 
 .PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial
 
-doc: doc-html doc-pdf doc-ps
+doc: doc-html doc-pdf doc-ps ide/index_urls.txt
 
 doc-html:\
   doc/tutorial/Tutorial.v.html doc/refman/html/index.html \