Fri, 04 May 2012 15:29:07 +0200 tags: line.rstrip().split() can be replaced with line.split()
Martin Geisler <mg@aragost.com> [Fri, 04 May 2012 15:29:07 +0200] rev 16589
tags: line.rstrip().split() can be replaced with line.split() The line looks like "123 <node> <node>" and does not start with whitespace: it was therefore not significant that rstrip was used instead of strip. Furthermore, the first part is fed to int, which will itself strip away whitespace before converting the string to an integer.
Fri, 04 May 2012 15:24:00 +0200 phases: line.strip().split() == line.split()
Martin Geisler <mg@aragost.com> [Fri, 04 May 2012 15:24:00 +0200] rev 16588
phases: line.strip().split() == line.split()
Sun, 06 May 2012 14:36:42 +0200 merge with stable
Martin Geisler <mg@lazybytes.net> [Sun, 06 May 2012 14:36:42 +0200] rev 16587
merge with stable
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip