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