tuned whitespace;
authorwenzelm
Mon, 27 May 2019 14:25:00 +0200
changeset 70292 bc9d02f916c4
parent 70291 9f3441164e92
child 70293 c7e9d3a0a681
tuned whitespace;
src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon May 27 12:05:16 2019 +0200
+++ b/src/Pure/General/file.ML	Mon May 27 14:25:00 2019 +0200
@@ -50,6 +50,7 @@
 val bash_path = Bash_Syntax.string o standard_path;
 val bash_paths = Bash_Syntax.strings o map standard_path;
 
+
 (* full_path *)
 
 fun full_path dir path =