Make $&time more precise and improve its time library handling #226
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is a smaller part of #210, which came from the discussion in #154. I'm not sure about the git history; this PR might be best merged squashed.
It's a fairly heavy refactor of
$&timewhich is, I think, quite a bit clearer, and does a better job than before of handling the messy set of time library functions available. It's not perfect --gettimeofday(3)is listed as "obsolescent" in the man page -- but swapping out functions is easy with the proposed setup.In part because of the better time library handling, it also reports times in milliseconds (real-time measurements might be in seconds on machines with don't have
gettimeofday(3), though I don't think there are a lot of those.)I'd still like those other changes from #210 at some point. This is just the part I feel actively impatient about: in my view, es
timeis almost useless without millisecond precision.