diff -r 2795499a20bd -r 9070a7c356c9 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Aug 30 15:52:09 2010 +0900
+++ b/src/Tools/Code/code_target.ML	Mon Aug 30 09:28:02 2010 +0200
@@ -13,7 +13,7 @@
   type literals = Code_Printer.literals
   val add_target: string * { serializer: serializer, literals: literals,
     check: { env_var: string, make_destination: Path.T -> Path.T,
-      make_command: string -> Path.T -> string -> string } } -> theory -> theory
+      make_command: string -> string -> string } } -> theory -> theory
   val extend_target: string *
       (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
     -> theory -> theory
@@ -116,7 +116,7 @@
 
 datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
       check: { env_var: string, make_destination: Path.T -> Path.T,
-        make_command: string -> Path.T -> string -> string } }
+        make_command: string -> string -> string } }
   | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
 
 datatype target = Target of {
@@ -336,7 +336,7 @@
         val destination = make_destination p;
         val _ = file destination (serialize thy target (SOME 80)
           (SOME module_name) args naming program names_cs);
-        val cmd = make_command env_param destination module_name;
+        val cmd = make_command env_param module_name;
       in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
         then error ("Code check failed for " ^ target ^ ": " ^ cmd)
         else ()