--- 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 =