diff options
| author | Hugo Herbelin | 2016-10-13 15:57:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-17 20:22:17 +0200 |
| commit | 57c6ffd23836364168ffd1c66dbddbecf830c7c6 (patch) | |
| tree | 051f302085ef8a33f90bd0533053d158e1b29b6d /doc/tutorial | |
| parent | 4204581ccb8bdf0f6c4298029c010c6deb643594 (diff) | |
Stopping warning on unrecognized unicode character in notation (fixing #5136).
The warning was pointless since the notation was accepted and parsed
anyway.
We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).
For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".
Diffstat (limited to 'doc/tutorial')
0 files changed, 0 insertions, 0 deletions