From dc8d33f4d3c010c657e61ba3e6b31d0e9d666f51 Mon Sep 17 00:00:00 2001
From: notin
Date: Sat, 25 Mar 2006 13:22:34 +0000
Subject: r8708@thot: notin | 2006-03-24 18:55:01 +0100 Correction d'un bug
sur la génération de la doc de stdlib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8662 85f007b7-540e-0410-9357-904b9bb8a0f7
---
doc/Makefile | 4 ++--
doc/stdlib/make-library-index | 7 +++++--
2 files changed, 7 insertions(+), 4 deletions(-)
(limited to 'doc')
diff --git a/doc/Makefile b/doc/Makefile
index e4b7e2fe97..d1998d4b16 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -207,7 +207,7 @@ faq/html/index.html: faq/FAQ.v.html
GLOBDUMP=$(COQTOP)/glob.dump
-LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap
+LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets
### Standard library (browsable html format)
@@ -220,7 +220,7 @@ stdlib/index-body.html: $(GLOBDUMP)
mv stdlib/html/index.html stdlib/index-body.html
stdlib/index-list.html: stdlib/index-list.html.template
- ./stdlib/make-library-index stdlib/index-list.html
+ COQTOP=$(COQTOP) ./stdlib/make-library-index stdlib/index-list.html
stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html
cat $^ > $@
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 1da642df31..ddbcd09fdf 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -6,7 +6,10 @@ FILE=$1
cp -f $FILE.template tmp
echo -n Building file index-list.prehtml ...
-for i in $COQTOP/theories/*; do
+
+for i in ../theories/*; do
+ echo $i
+
d=`basename $i`
if [ "$d" != "Num" -a "$d" != "CVS" ]; then
for j in $i/*.v; do
@@ -15,7 +18,7 @@ for i in $COQTOP/theories/*; do
grep -q theories/$d/$b.v tmp
a=$?
if [ $a = 0 ]; then
- sed -e "s/theories\/$d\/$b.v/$b<\/a>/g" tmp > tmp2
+ sed -e "s:theories/$d/$b.v:$b:g" tmp > tmp2
mv -f tmp2 tmp
else
echo Warning: theories/$d/$b.v is missing in the template file
--
cgit v1.2.3