This value of this option is a function that takes a filename f and a command string c as its two parameters, and returns a string that, when run, will execute c and put statistics in f.
The default function should work in most cases. It first tries to use /usr/bin/time, then the time implementation built-in to certain shells, and otherwise makes the feature unavailable. Certain implementations of /usr/bin/time are given special flags to provide more details.
The object KeepStatisticsCommand is a symbol.