diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 17:14:43 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 17:14:43 +0000 |
commit | 16accd57086a56f42cc5d2d18b3f0de8faeecdbd (patch) | |
tree | 3cb1de4e5c23d59b235e480650614791ae1ce5aa /debian | |
parent | f83c83e2a64e5bc5b9b1f5afecb3c461d90bb6b9 (diff) |
Document the patch.
Diffstat (limited to 'debian')
-rwxr-xr-x | debian/patches/coqdoc_stdlib.dpatch | 3 |
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 |