use TMPDIR for buildbot

slefrancois · slefrancois · commit 31e194d4a844 · 2016-09-09T15:45:53.000-04:00
diff --git a/misc/do_nightly_build b/misc/do_nightly_build
@@ -2,7 +2,10 @@
 
 # If not jenkins, set workspace to local Tmp
 if [ -v $WORKSPACE ]; then
-   WORKSPACE=/Tmp
+   if [ -v $TMPDIR ]; then
+      TMPDIR=/tmp
+   fi
+   WORKSPACE=$TMPDIR
 fi
 
 date
