# HG changeset patch
# User wenzelm
# Date 1577125657 -3600
# Node ID 6d9dd5309b85774341539fe73656ccf99dfaa7ac
# Parent  05400628c56b3ac64c59444d4c354141078d1575
proper File.platform_path for Windows;

diff -r 05400628c56b -r 6d9dd5309b85 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Dec 23 19:07:25 2019 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Dec 23 19:27:37 2019 +0100
@@ -40,7 +40,9 @@
 
         val (output, rc) =
           Isabelle_System.bash_output
-            ("\"$ISABELLE_CSDP\" " ^ File.bash_path in_path ^ " " ^ File.bash_path out_path)
+            ("\"$ISABELLE_CSDP\" " ^
+              Bash.string (File.platform_path in_path) ^ " " ^
+              Bash.string (File.platform_path out_path));
         val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
 
         val result = if File.exists out_path then File.read out_path else ""