From 9a049cb107efab5b03dae694d8c7bf9b97655450 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Mon, 23 Sep 2013 18:46:09 +0100 Subject: [PATCH] goaljobs: sh: ~tmpdir default should be true not false. --- goaljobs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/goaljobs.ml b/goaljobs.ml index 94843ac..489f387 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 -- 1.8.3.1