Accept URLs of form file:/home... also.
authoraspinall
Thu Nov 23 22:14:26 2006 +0100 (2006-11-23 ago)
changeset 21503c4ea7e8c3937
parent 21502 7f3ea2b3bab6
child 21504 9c97af4a1567
Accept URLs of form file:/home... also.
src/Pure/General/url.ML
     1.1 --- a/src/Pure/General/url.ML	Thu Nov 23 20:34:21 2006 +0100
     1.2 +++ b/src/Pure/General/url.ML	Thu Nov 23 22:14:26 2006 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4    Scan.this_string "file:///" |-- scan_path_root >> File ||
     1.5    Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
     1.6    Scan.this_string "file://" |-- scan_host -- scan_path >> RemoteFile ||
     1.7 +  Scan.this_string "file:/" |-- scan_path_root >> File ||
     1.8    Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
     1.9    Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
    1.10