diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-03 10:12:13 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-03 10:26:31 +0100 |
commit | 6243a0b9c16562a90e0e14f60047e9b0f2a0f2e8 (patch) | |
tree | 37b6a1c7009975b2608978a37c80bf489ca9ba4c /plugins/syntax/ascii_syntax.ml | |
parent | 4fb06717f96ce761dbe20f781128609cf41f9bef (diff) |
Fix error reporting id on VtUnknown commands
Diffstat (limited to 'plugins/syntax/ascii_syntax.ml')
0 files changed, 0 insertions, 0 deletions