tools: ssh: Minor change on ssh run tool script.

tools/ssh-run.sh

@@ -1,10 +1,14 @@
 #! /bin/sh
 
-# > ssh-run.sh SERVER DESTDIR SOLVER INPUT
+# > ssh-run.sh SERVER DESTDIR SOLVER ARGS INPUT
 
 # First argument is the server name/addr
 # The second argument is the destination directory to copy input data
 # The third argument is the solver path
-# The fourth argument is the input name
+# The fourth argument is an solver args separate by ',' or input name
+# The sixth argument is the input name or nothing
 
-ssh $1 "cd $2; $3 $4"
+args=$(echo $4 | tr ',' ' ')
+
+echo "ssh $1 \"cd $2; $3 $args $5\""
+ssh $1 "cd $2; $3 $args $5"