src/Pure/General/file.ML
changeset 8163 0b5be7287661
parent 7850 3689adcf9b8b
child 8806 a202293db3f6
equal deleted inserted replaced
8162:020e384e67dd 8163:0b5be7287661
    98   if system cmd <> 0 then error ("System command failed: " ^ cmd)
    98   if system cmd <> 0 then error ("System command failed: " ^ cmd)
    99   else ();
    99   else ();
   100     
   100     
   101 fun mkdir path = system_command ("mkdir -p " ^ quote_sysify path);
   101 fun mkdir path = system_command ("mkdir -p " ^ quote_sysify path);
   102 
   102 
   103 fun copy_all path1 path2 =
   103 fun copy_all path1 path2 =  (*dereferences symlinks!*)
   104   system_command ("cp -R " ^ quote_sysify path1 ^ " " ^ quote_sysify path2);
   104   system_command ("cp -r " ^ quote_sysify path1 ^ " " ^ quote_sysify path2);
   105 
   105 
   106 
   106 
   107 (* symbol_use *)
   107 (* symbol_use *)
   108 
   108 
   109 val plain_use = use o sysify_path;
   109 val plain_use = use o sysify_path;