From: Johannes Schindelin <hidden> Date: 2017-01-07 10:51:44
Hi Peff,
On Sat, 7 Jan 2017, Jeff King wrote:
On Fri, Jan 06, 2017 at 01:04:05AM -0800, Brandon Tolsch wrote:
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.
Ciao,
Dscho