diff options
| author | herbelin | 2010-04-09 08:54:04 +0000 |
|---|---|---|
| committer | herbelin | 2010-04-09 08:54:04 +0000 |
| commit | 30488fec6d5c4b78aa3f338be0e6b69f99a4590c (patch) | |
| tree | cf4987f5d0b32e7e97f07425908f67ab5308c3e6 /dev/base_include | |
| parent | 69b757baefaddb9d32978d06044c8005f38aa337 (diff) | |
Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing
rules (bug report #2293).
Restored the sequential extension of the printing rules tables (that
commit #12905 replaced by a per-file modification of the printing
rules table). Note however that the table grows in the order of
compilation of files by coqdoc, which does not necessarily coincide
with the order of coqc compilation dependencies of the files.
Added documentation of coqdoc option "--external".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions