# HG changeset patch # User aspinall # Date 1164316466 -3600 # Node ID c4ea7e8c39370179d551b4fdf8ec4e3bf0de6b47 # Parent 7f3ea2b3bab66706341786bc2ba53b734aa63afb Accept URLs of form file:/home... also. diff -r 7f3ea2b3bab6 -r c4ea7e8c3937 src/Pure/General/url.ML --- a/src/Pure/General/url.ML Thu Nov 23 20:34:21 2006 +0100 +++ b/src/Pure/General/url.ML Thu Nov 23 22:14:26 2006 +0100 @@ -65,6 +65,7 @@ Scan.this_string "file:///" |-- scan_path_root >> File || Scan.this_string "file://localhost/" |-- scan_path_root >> File || Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile || + Scan.this_string "file:/" |-- scan_path_root >> File || Scan.this_string "http://" |-- scan_host -- scan_path >> Http || Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;