On Sat, Jan 07, 2017 at 11:51:23AM +0100, Johannes Schindelin wrote:
quoted
We can fix this by making the ".*" less greedy. Instead of
depending on ".*?" working portably, we can just limit the
match to non-digit characters, which accomplishes the same
thing.
Or we could simply require a space before the first digit, which would
maybe look a little simpler.
Yeah, if we can assume that all translations will always have a space
there. It is almost certainly true for Western languages, but I don't
know about others. It looks like the Korean translation omits a space
_after_ the digits, but there is still one before.
-Peff