1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules
index f23efc82..550349dd 100755
--- a/debian/rules
+++ b/debian/rules
@@ -44,7 +44,7 @@ build-stamp:
 	fi
 	$(MAKE) glob.dump
 	cp tools/coqdoc/coqdoc.sty doc/stdlib/
-	$(MAKE) -C doc stdlib
+	$(MAKE) -C doc stdlib/html/index.html
 	touch build-stamp
 
 clean: unpatch