changeset: 3505:ab6a712c7eb6 tag: tip user: Ian Hinder <ian.hinder at aei.mpg.de> date: Wed Apr 04 13:14:38 2012 +0200 summary: Make timer tree output precision and threshold configurable with parameters