diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-27 19:46:40 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-27 19:46:49 +0100 |
| commit | f3ff16adced3e5bf8d11cb74ee68be1267edc2b6 (patch) | |
| tree | 8c6d9cfeedd2dc391b03c77a09c60a276f17a0a7 /test-suite/bugs/closed/4165.v | |
| parent | e8b4756c655eacd8a2b9b23630ba02dbbbc4e96e (diff) | |
Normalize scope names before storing them in vo files. (Fix for bug #4162)
Note that I do not understand why the delimiter map is incomplete on
loading and thus was causing a failure. So, while the patch is the proper
way to deal with notation scopes, there might be another bug lurking in
this file.
Diffstat (limited to 'test-suite/bugs/closed/4165.v')
0 files changed, 0 insertions, 0 deletions