# HG changeset patch
# User wenzelm
# Date 1558959900 -7200
# Node ID bc9d02f916c4610882cf63a9ba342fb748156384
# Parent  9f3441164e9255b1a7c6e7e444c3c5c1d6697b98
tuned whitespace;

diff -r 9f3441164e92 -r bc9d02f916c4 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 =