summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 17:14:43 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 17:14:43 +0000
commit16accd57086a56f42cc5d2d18b3f0de8faeecdbd (patch)
tree3cb1de4e5c23d59b235e480650614791ae1ce5aa
parentf83c83e2a64e5bc5b9b1f5afecb3c461d90bb6b9 (diff)
Document the patch.
-rwxr-xr-xdebian/patches/coqdoc_stdlib.dpatch3
1 files changed, 2 insertions, 1 deletions
diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
index d81ce3c8..a2530876 100755
--- a/debian/patches/coqdoc_stdlib.dpatch
+++ b/debian/patches/coqdoc_stdlib.dpatch
@@ -2,7 +2,8 @@
## coqdoc_stdlib.dpatch by Samuel Mimram <smimram@debian.org>
##
## All lines beginning with `## DP:' are a description of the patch.
-## DP: No description.
+## DP: Add an option to coqdoc to be able to use a custom stdlib path in order
+## DP: to be able to build the documentation before coqdoc is installed.
@DPATCH@
diff -urNad coq-8.0pl3+8.1alpha~/doc/Makefile coq-8.0pl3+8.1alpha/doc/Makefile