diff --git a/ressources/init_repl.sh b/ressources/init_repl.sh index eb51dbec..45f8a6c0 100755 --- a/ressources/init_repl.sh +++ b/ressources/init_repl.sh @@ -35,7 +35,7 @@ mkfifo $working_dir/$pipe touch $working_dir/$out sleep 36000 > $working_dir/$pipe & -echo "/bin/cat " $working_dir/$pipe " | " $repl > $working_dir/real_launcher.sh +echo "\cat " $working_dir/$pipe " | " $repl > $working_dir/real_launcher.sh chmod +x $working_dir/real_launcher.sh echo $repl " process started at $(date +"%F %T")." >> $log diff --git a/ressources/launcher_repl.sh b/ressources/launcher_repl.sh index feaa91e7..23da816e 100755 --- a/ressources/launcher_repl.sh +++ b/ressources/launcher_repl.sh @@ -1,2 +1,2 @@ #!/bin/bash -/bin/cat $1 > $2 +\cat $1 > $2