src/Pure/General/file.ML
changeset 18715 f809deffdd8f
parent 18678 dd0c569fa43d
child 19473 d87a8838afa4
equal deleted inserted replaced
18714:1c310b042d69 18715:f809deffdd8f
   145   (system_command ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); ()))
   145   (system_command ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); ()))
   146 
   146 
   147 
   147 
   148 (* use ML files *)
   148 (* use ML files *)
   149 
   149 
   150 val use = Output.toplevel_errors (use o platform_path);
   150 val use = Output.ML_errors use o platform_path;
   151 
   151 
   152 end;
   152 end;