Dune::Timer measures wall-time unlike it is documented
The documentation of
Dune::Timer states it measures elapsed user-time. Since fa43f4bf Dune::Timer uses
std::chrono::high_resolution_clock, which measures wall-time.
I don't find any documentation nor occurrence (except in timer.hh) of the switch
TIMER_USE_STD_CLOCK. Should it be set by the user?