1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 15:52:09 2010 +0900
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 09:28:02 2010 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    type literals = Code_Printer.literals
     1.5    val add_target: string * { serializer: serializer, literals: literals,
     1.6      check: { env_var: string, make_destination: Path.T -> Path.T,
     1.7 -      make_command: string -> Path.T -> string -> string } } -> theory -> theory
     1.8 +      make_command: string -> string -> string } } -> theory -> theory
     1.9    val extend_target: string *
    1.10        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    1.11      -> theory -> theory
    1.12 @@ -116,7 +116,7 @@
    1.13  
    1.14  datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
    1.15        check: { env_var: string, make_destination: Path.T -> Path.T,
    1.16 -        make_command: string -> Path.T -> string -> string } }
    1.17 +        make_command: string -> string -> string } }
    1.18    | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    1.19  
    1.20  datatype target = Target of {
    1.21 @@ -336,7 +336,7 @@
    1.22          val destination = make_destination p;
    1.23          val _ = file destination (serialize thy target (SOME 80)
    1.24            (SOME module_name) args naming program names_cs);
    1.25 -        val cmd = make_command env_param destination module_name;
    1.26 +        val cmd = make_command env_param module_name;
    1.27        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.28          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.29          else ()