-
Robert Ricci authored
Is controlled by a new configure variable called TIMESTAMPS - if this variable is set, prints out a timestamp, along with its arguments (so that you can distinguish between the timesteamps.) Otherwise, does nothing. The basic idea is that we can sprinkle calls to this in the code, and only enable it on devel trees.
29edb522