equal
deleted
inserted
replaced
690 (*timed "use" function, printing filenames*) |
690 (*timed "use" function, printing filenames*) |
691 fun time_use fname = timeit (fn () => |
691 fun time_use fname = timeit (fn () => |
692 (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname; |
692 (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname; |
693 writeln ("\n**** Finished " ^ fname ^ " ****"))); |
693 writeln ("\n**** Finished " ^ fname ^ " ****"))); |
694 |
694 |
|
695 (*For Makefiles: use the file, but exit with error code if errors found.*) |
|
696 fun exit_use fname = use fname handle _ => exit 1; |
695 |
697 |
696 |
698 |
697 (** filenames **) |
699 (** filenames **) |
698 |
700 |
699 (*convert UNIX filename of the form "path/file" to "path/" and "file"; |
701 (*convert UNIX filename of the form "path/file" to "path/" and "file"; |