# HG changeset patch
# User wenzelm
# Date 1204835547 -3600
# Node ID b8bbbb76220c621a71917fecbefea02e874f0cbc
# Parent  58790194116c796a806344706b2a84e9c4f27fcb
replaced execute by system_out;

diff -r 58790194116c -r b8bbbb76220c src/HOL/Matrix/cplex/Cplex_tools.ML
--- 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