9313970 save execution time in extra args instead note

Authored and Committed by kparal 6 years ago
    save execution time in extra args instead note
    
    Note is very visible for the end user and execution time is distracting
    and not useful for them. Save it in extra args. As an added benefit, it
    can be used to query results, and it can be easily processed (retrieve
    results and then sort them by execution time) without parsing.
    
        
file modified
+3 -2