author | wenzelm |
Thu, 06 Mar 2008 21:32:27 +0100 | |
changeset 26228 | b8bbbb76220c |
parent 26227 | 58790194116c |
child 26229 | 116d3cfc0d89 |
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Mar 06 21:13:11 2008 +0100 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Thu Mar 06 21:32:27 2008 +0100 @@ -1146,7 +1146,7 @@ val cplex_path = getenv "GLPK_PATH" val cplex = if cplex_path = "" then "glpsol" else cplex_path val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname) - val answer = execute command + val answer = #1 (system_out command) in let val result = load_glpkResult resultname