]> ocean-lang.org Git - ocean/commitdiff
scanner: handle completely unrecognized characters.
authorNeilBrown <neil@brown.name>
Wed, 29 May 2019 08:25:50 +0000 (18:25 +1000)
committerNeilBrown <neil@brown.name>
Wed, 29 May 2019 08:25:50 +0000 (18:25 +1000)
If we are ignoring numbers, then a digit looks like
nothing at all, not even an unknown mark.
Make sure to handle that properly.

Signed-off-by: NeilBrown <neil@brown.name>

No differences found