diff --git a/tools/times.sh b/tools/times.sh index ca0e60bd9..110d96b37 100755 --- a/tools/times.sh +++ b/tools/times.sh @@ -1,6 +1,6 @@ #!/bin/bash # -# Simple script to generate times.log that contains timing information for the last 20 revisions +# Simple script to generate times.log that contains timing information for the last revisions # Typically these commands shall be used to get times.txt: mkdir -p src cp lib/* src/ # fill src/ with some source code