aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-01-31 00:54:06 +0100
committerHugo Herbelin2020-03-03 17:35:52 +0100
commit154aeaad0802e621d09048e1e32485946a3ec443 (patch)
tree798f4f551f6b2cc151a8a2ecca8710cf8eff0d86 /kernel/genOpcodeFiles.ml
parent18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (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