diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-17 19:59:39 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-17 19:59:39 +0000 |
commit | 2521bbc7e9805fd57d2852c1e9631250def11d57 (patch) | |
tree | 6cdc089a8a07a033bc5089edb5bbaa3adb193412 /dev/ocamlopt_shared_os5fix.sh | |
parent | d25dfc1a30ab227178f8cd4304f28a35f4d7e19d (diff) |
About "unsupported" unicode characters in notations.
- 8.2 (bug-fix): reverted check for unicode early at notation definition time
(an unsupported "cadratin" space, 0x2003, was used in CoRN!) [by the way,
what to do with unicode spacing characters in general?]
- trunk: improved error message, removed redundant code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/ocamlopt_shared_os5fix.sh')
0 files changed, 0 insertions, 0 deletions