merge benchmark changes
authorChristian Grothoff <christian@grothoff.org>
Mon, 4 Jun 2018 17:17:57 +0000 (19:17 +0200)
committerChristian Grothoff <christian@grothoff.org>
Mon, 4 Jun 2018 17:17:57 +0000 (19:17 +0200)
commitb670eec1c0ea387ae31b52dd0d51c1422949a55c
tree5abaffddad0c258e6b166ada4ef3fb97ba51b5d1
parent2b99bddcb6961cfda34087138acdda4b8b9ccb9f
parent41cbe10b783a0741c75566232886f262cd779fbb
merge benchmark changes