From fe730babfe0c01baa6c6da62460938f8839aa7c6 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sun, 30 Apr 2006 14:17:58 +0000
Subject: Correct the FTBFS because of LaTeX.

---
 debian/rules | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'debian/rules')

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
-- 
cgit v1.2.3