diff --git a/scripts/profile_output.py b/scripts/profile_output.py index 135c8566..ff317dea 100755 --- a/scripts/profile_output.py +++ b/scripts/profile_output.py @@ -18,11 +18,26 @@ Options: import time import profile +import pstats from docopt import docopt import jedi +# Monkeypatch the time formatting function of profiling to make it easier to +# understand small time differences. +def f8(x): + ret = "%7.3f " % x + if ret == ' 0.000 ': + return "%6dµs" % (x * 10000000) + if ret.startswith(' 0.00'): + return "%8.4f" % x + return ret + + +pstats.f8 = f8 + + def run(code, index, infer=False): start = time.time() script = jedi.Script(code)