| Mon, 09 Mar 2020 19:35:07 +0100 |
wenzelm |
more scalable output of YXML files;
|
file |
diff |
annotate
|
| Wed, 15 Jan 2020 13:22:16 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 14 Nov 2019 11:35:02 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 16:01:44 +0100 |
wenzelm |
more thorough File.set_executable, notably for Windows;
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 15:45:40 +0100 |
wenzelm |
added executable flag for exports;
|
file |
diff |
annotate
|
| Thu, 20 Dec 2018 22:56:36 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2018 21:13:47 +0100 |
wenzelm |
clarified operations: uniform sorting of results;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2018 22:46:44 +0100 |
wenzelm |
more direct File.executable operation: avoid external process (on Unix);
|
file |
diff |
annotate
|
| Wed, 05 Dec 2018 21:15:18 +0100 |
wenzelm |
more direct File.link operation: avoid external process;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2018 14:59:42 +0100 |
wenzelm |
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
|
file |
diff |
annotate
|
| Wed, 14 Nov 2018 20:04:39 +0100 |
wenzelm |
more uniform find_files, notably for symlinks;
|
file |
diff |
annotate
|
| Wed, 14 Nov 2018 16:26:58 +0100 |
wenzelm |
is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
|
file |
diff |
annotate
|
| Wed, 14 Nov 2018 11:51:03 +0100 |
wenzelm |
clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
|
file |
diff |
annotate
|
| Tue, 13 Nov 2018 12:37:46 +0100 |
wenzelm |
clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
|
file |
diff |
annotate
|
| Tue, 26 Sep 2017 16:12:21 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|