From a47e2f6587e3507a12d4d86b9769b93e01023350 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 17 Jan 2020 01:25:06 +0100
Subject: [doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]

This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.
---
 doc/stdlib/make-library-index | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'doc/stdlib/make-library-index')

diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index bea6f24098..732f15b78a 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 # Instantiate links to library files in index template
 
@@ -8,9 +8,14 @@ HIDDEN=$2
 cp -f $FILE.template tmp
 echo -n "Building file index-list.prehtml... "
 
-LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native`
+LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native`
 
 for k in $LIBDIRS; do
+    if [[ $k =~ "user-contrib" ]]; then
+        BASE_PREFIX=""
+    else
+        BASE_PREFIX="Coq."
+    fi
     d=`basename $k`
       ls $k | grep -q \.v'$'
       if [ $? = 0 ]; then
@@ -26,7 +31,7 @@ for k in $LIBDIRS; do
                     echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1
                 else
 		    p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'`
-		    sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		    sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2
 		    mv -f tmp2 tmp
                 fi
 	    else
-- 
cgit v1.2.3