Thanks. I pushed this.
--Justin
On Jan 5, 2012, at 11:04 AM, Ben Pfaff wrote:
> Thanks, I pushed this to master.
>
> On Wed, Jan 04, 2012 at 11:10:23PM -0800, Justin Pettit wrote:
>> Looks good. Thanks.
>>
>> --Justin
>>
>>
>> On Jan 4, 2012, at 4:12 PM, Ben Pfaff wrote:
>>
>>> The "sed"
Thanks, I pushed this to master.
On Wed, Jan 04, 2012 at 11:10:23PM -0800, Justin Pettit wrote:
> Looks good. Thanks.
>
> --Justin
>
>
> On Jan 4, 2012, at 4:12 PM, Ben Pfaff wrote:
>
> > The "sed" command here is intended to replace something like 1234...1234
> > (where the two numbers are t
Looks good. Thanks.
--Justin
On Jan 4, 2012, at 4:12 PM, Ben Pfaff wrote:
> The "sed" command here is intended to replace something like 1234...1234
> (where the two numbers are the same) with and something like
> 1234...2345 (where the two numbers differ) with , but in fact it
> accidentally
The "sed" command here is intended to replace something like 1234...1234
(where the two numbers are the same) with and something like
1234...2345 (where the two numbers differ) with , but in fact it
accidentally changed, e.g., 10...1016 into 16. This commit fixes
that.
This fixes only a test cas