From 80b5ceadd16e566c944cd8c48ffc486caca3d6a9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Dec 2015 13:46:31 +0100
Subject: some doc for the doc building utility

---
 etc/utils/builddoc_lib.sh | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'etc/utils')

diff --git a/etc/utils/builddoc_lib.sh b/etc/utils/builddoc_lib.sh
index 89d1911..0ab4fbd 100644
--- a/etc/utils/builddoc_lib.sh
+++ b/etc/utils/builddoc_lib.sh
@@ -60,6 +60,9 @@ sed -r -e '
 done
 }
 
+# example invocation:
+# MAKEDOT=../etc/utils/ PATH=$COQBIN:$PATH MANGLEDOT=touch COQDOCOPTS="-R . mathcomp" \
+#	build_doc */*.v
 build_doc() {
 rm -rf html
 mkdir html
-- 
cgit v1.2.3