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/stdlib/make-library-index | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'doc/stdlib')

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/<a href=\"Coq.$d.$b.html\">$b<\/a>/g" tmp > tmp2
+      sed -e "s:theories/$d/$b.v:<a href=\"Coq.$d.$b.html\">$b</a>:g" tmp > tmp2
       mv -f tmp2 tmp
     else
       echo Warning: theories/$d/$b.v is missing in the template file
-- 
cgit v1.2.3