Diffusion nofib 35fc121fc8cc

Fix: #12084 deprecate old profiling flags

Authored by seraphime on May 22 2016, 10:47 AM.

Description

Fix: Trac #12084 deprecate old profiling flags

Details

Committed
thomieMay 22 2016, 12:23 PM
Parents
rNOFIBdfa9f9158943: De-tab CmdLine.hs
Branches
Unknown
Tags
Unknown