Permalink
Browse files

remove a bash-ism from HolQbfLib

When /bin/sh is dash (e.g. on Ubuntu I think) HolQbfLib's system call to
squolem2 won't work ("Syntax error: Bad fd number"). This should fix it.
  • Loading branch information...
1 parent ec954cf commit d24a68ee55c80fec23e7a7e8eecb0df0ec29250d @xrchz xrchz committed Oct 11, 2011
Showing with 1 addition and 1 deletion.
  1. +1 −1 src/HolQbf/HolQbfLib.sml
View
2 src/HolQbf/HolQbfLib.sml
@@ -9,7 +9,7 @@ structure HolQbfLib :> HolQbfLib = struct
val path = FileSys.tmpName ()
val dict = QDimacs.write_qdimacs_file path t
(* the actual system call to Squolem *)
- val cmd = "squolem2 -c " ^ path ^ " >& /dev/null"
+ val cmd = "squolem2 -c " ^ path ^ " >/dev/null 2>&1"
val _ = if !QbfTrace.trace > 1 then
Feedback.HOL_MESG ("HolQbfLib: calling external command '" ^ cmd ^ "'")
else ()

0 comments on commit d24a68e

Please sign in to comment.