Merge pull request #272 from GaetanLepage/cat

ressources: use \cat instead of /bin/cat in scripts
michaelb · Jan 16, 2024 · b2b6f13 · b2b6f13
2 parents b3254d8 + c5c3d87
commit b2b6f13
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -1,2 +1,2 @@
 #!/bin/bash
-/bin/cat $1 > $2
+\cat $1 > $2