diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-12 19:29:24 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-12 19:29:24 +0000 |
| commit | 21255e54d92ba5b9dcc98f634329ec58618b1540 (patch) | |
| tree | ceef44e872f2a2529254f440f44fa70247583c5b /Makefile.doc | |
| parent | 471e50d415a30191f0ebdaa707ce1889990d4923 (diff) | |
Correction d'un problème lié à une interaction entre hyperref et
latex, qui empechait de produire des fichiers .dvi à partir des .tex
générés par coqdoc.
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M trunk/tools/coqdoc/coqdoc.sty
M branches/v8.2/tools/coqdoc/coqdoc.sty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions