diff options
| author | herbelin | 2010-03-30 19:17:33 +0000 |
|---|---|---|
| committer | herbelin | 2010-03-30 19:17:33 +0000 |
| commit | 358e5b1daef7ec1681092f8b1888b57da078a8b6 (patch) | |
| tree | 662304d151d58972780517623316e15708b5f87f | |
| parent | e7d037bf195e02a3a17d34ab7bd08f0e12689664 (diff) | |
Removed hard-wiring of latin1 letters in coqdoc (see bug #2275)
(it interfered badly with utf-8: just take an utf-8 like "forall" which
starts in iso-8859-1 with a "a circonflex"; nothing is lost since
intentedly iso-8859-1 chars can only occur in comments and there is no
ident detection in comments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12895 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 95ad1c1139..779d10e99d 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -264,10 +264,8 @@ let space_nl = [' ' '\t' '\n' '\r'] let nl = "\r\n" | '\n' let firstchar = - ['A'-'Z' 'a'-'z' '_' - (* iso 8859-1 accents *) - '\192'-'\214' '\216'-'\246' '\248'-'\255' ] | - (* *) + ['A'-'Z' 'a'-'z' '_'] | + (* superscript 1 *) '\194' '\185' | (* utf-8 latin 1 supplement *) '\195' ['\128'-'\191'] | |