Summary
- tuned signature;
- more operations for profiling;
- provide rsync component, with uniform version + options on all platforms;
- tuned message;
- provide local component to remote directory;
- tuned output;
- more SSH operations;
- more operations;
- tuned comments;
- clarified directory names, following bash_process (see e59d7d6fe1bd);
- tuned README;
- clarified build options;
The file was modified | src/Pure/context.ML (diff) |
The file was modified | src/Pure/ML/ml_heap.ML (diff) |
The file was modified | Admin/components/components.sha1 (diff) |
The file was modified | Admin/components/main (diff) |
The file was modified | src/Pure/Admin/component_rsync.scala (diff) |
The file was modified | src/Pure/System/components.scala (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | src/Pure/General/ssh.scala (diff) |
The file was modified | src/Pure/System/components.scala (diff) |
The file was modified | src/Pure/Thy/sessions.scala (diff) |
The file was modified | src/Pure/Admin/component_rsync.scala (diff) |
The file was modified | src/Pure/Admin/component_lipics.scala (diff) |
The file was modified | src/Pure/Admin/component_rsync.scala (diff) |
The file was modified | src/Pure/Admin/component_rsync.scala (diff) |
The file was modified | src/Pure/Admin/component_rsync.scala (diff) |