Merge pull request #4979 from davidbrai/allow-parse_log-to-skip-lines
authorEvan Shelhamer <shelhamer@imaginarynumber.net>
Fri, 18 Nov 2016 17:46:25 +0000 (09:46 -0800)
committerGitHub <noreply@github.com>
Fri, 18 Nov 2016 17:46:25 +0000 (09:46 -0800)
Support solver resumes in parse_log.py


Trivial merge