diff options
| author | sacerdot | 2004-04-05 17:19:24 +0000 |
|---|---|---|
| committer | sacerdot | 2004-04-05 17:19:24 +0000 |
| commit | 986aacb2b2e0b15d76c9b9691ad89da14f462a5d (patch) | |
| tree | ca5af0efa9ba05371b4117a9e59f787b3863bc54 /dev/base_include | |
| parent | cfff5f57ff1e956e5a332ff466638db420474d7a (diff) | |
Since coqdoc produces (X)HTML, HTML character entities can be used
in .v files. The exportation module produces generic XML ==> the character
entities that were verbatim copied were never declared and the generated
files were not well-formed XML files. Fixed by adding to the internal subset
of the DTD an inclusion to the three files were the (X)HTML entities are
defined. Due to technical reasons (HELM Getter URL rewriting), the chosen
URL refers to the HELM web site.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5636 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions