# HG changeset patch
# User wenzelm
# Date 939836403 -7200
# Node ID 3689adcf9b8bef4c7892f0336aeb5f28123f878d
# Parent  29a2a1d71128f77182b2f293514eccb67153712e
mkdir, copy_all: system_command;

diff -r 29a2a1d71128 -r 3689adcf9b8b src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Oct 13 19:39:19 1999 +0200
+++ b/src/Pure/General/file.ML	Wed Oct 13 19:40:03 1999 +0200
@@ -94,10 +94,14 @@
 
 val quote_sysify = enclose "'" "'" o sysify_path;
 
-fun mkdir path = (execute ("mkdir -p " ^ quote_sysify path); ());
+fun system_command cmd =
+  if system cmd <> 0 then error ("System command failed: " ^ cmd)
+  else ();
+    
+fun mkdir path = system_command ("mkdir -p " ^ quote_sysify path);
 
 fun copy_all path1 path2 =
-  (execute ("cp -R " ^ quote_sysify path1 ^ " " ^ quote_sysify path2); ());
+  system_command ("cp -R " ^ quote_sysify path1 ^ " " ^ quote_sysify path2);
 
 
 (* symbol_use *)