Fix "the input device is not a TTY" with non-interactive commands

Fixes running non-interactive commands via plain ssh (as opposed to
"ssh -t"):

  $ ssh server /path/to/isolate-gpu -d 0 echo hello
  the input device is not a TTY

... by avoiding to pass "-it" to "docker run" if we don't have a
terminal.  We now get the expected:

  $ ssh server /path/to/isolate-gpu -d 0 echo hello
  hello

Author: palves

isolate-gpu

@@ -190,7 +190,17 @@ for group_id in "${groups_array[@]}"; do
     group_add_options+=(--group-add "$group_id")
 done
 
-docker run -it --rm \
+EXTRA_OPTS=()
+
+# Go interactive iff we have a terminal.  This avoids "The input
+# device is not a TTY" errors when running a non-interactive session
+# via ssh.  E.g., "ssh server isolate-gpu -d 0 make -C project-dir".
+if [ -t 1 ]; then
+    EXTRA_OPTS+=(-ti)
+fi
+
+docker run --rm \
+       "${EXTRA_OPTS[@]}" \
        -u "$(id -u):$(id -g)" \
        "${group_add_options[@]}" \
        --cap-add=SYS_PTRACE \