summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xdebian/rules2
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules
index a9bd3b67..5151c911 100755
--- a/debian/rules
+++ b/debian/rules
@@ -51,7 +51,7 @@ build-stamp: patch-stamp configure-stamp
$(MAKE) BEST=byte HASCOQIDE=byte glob.dump; \
fi
cp tools/coqdoc/coqdoc.sty doc/stdlib/
- $(MAKE) -C doc stdlib/html/index.html
+ $(MAKE) -f Makefile.stage3 doc/stdlib/html/index.html COQDOC="bin/coqdoc --coqlib_path `pwd`"
touch build-stamp
clean: unpatch