search for: 516cff3

Unix.gettimeofday returns a finer resolution than seconds, which is what we need since deciseconds of timestamps are printed. --- mllib/common_utils.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mllib/common_utils.ml b/mllib/common_utils.ml index 32e908d..516cff3 100644 --- a/mllib/common_utils.ml +++ b/mllib/common_utils.ml @@ -282,11 +282,11 @@ let verbose () = !verbose (* Timestamped progress messages, used for ordinary messages when not * --quiet. *) -let start_t = Unix.time () +let start_t = Unix.gettimeofday () let message fs = let display st...

This way it is possible to use rm_rf_only_files, but not removing specific files. --- mllib/common_utils.ml | 8 +++++++- mllib/common_utils.mli | 5 ++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/mllib/common_utils.ml b/mllib/common_utils.ml index 516cff3..3737b4c 100644 --- a/mllib/common_utils.ml +++ b/mllib/common_utils.ml @@ -640,13 +640,19 @@ let rmdir_on_exit = * without removing the actual directory structure. Also if 'dir' is * not a directory or doesn't exist, ignore it. * + * The optional filter is used to filter out fil...