diff --git a/goaljobs.ml b/goaljobs.ml index 94843acb97126264005c83b6c0a79e866e9c24fd..489f38743ab65028cb0ab9ed4172b650ed7a5d66 100644 --- a/goaljobs.ml +++ b/goaljobs.ml @@ -242,7 +242,7 @@ let rm_rf dir = let shell = ref "/bin/sh" (* Used by sh, shout, shlines to handle the script and temporary dir. *) -let with_script ?(tmpdir = false) script f = +let with_script ?(tmpdir = true) script f = let dir = if tmpdir then Some (make_tmpdir ()) else None in let script_file, chan = match dir with