diff options
| author | Hugo Herbelin | 2020-01-31 00:54:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-03 17:35:52 +0100 |
| commit | 154aeaad0802e621d09048e1e32485946a3ec443 (patch) | |
| tree | 798f4f551f6b2cc151a8a2ecca8710cf8eff0d86 /kernel/genOpcodeFiles.ml | |
| parent | 18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff) | |
When parsing negative integer, ensure minus sign is contiguous to the number.
For instance, formerly, "Set Inline Level - 1" was succeeding. Now
only "Set Inline Level -1" succeeds. (Even though -1 does not make
sense for a Inline Level, but that's then a semantic issue. Other
options may accept negative numbers in general.)
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions
