From d6c7661cea5a874663179d806199634b7c4076ed Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 28 Jul 2008 16:02:40 +0200 Subject: Fix building of (stdlib) doc --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian/rules') 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 -- cgit v1.2.3