From c5c3d877f9f1966a1d37fb91828722fa9515300b Mon Sep 17 00:00:00 2001
From: Gaetan Lepage <gaetan@glepage.com>
Date: Sat, 30 Dec 2023 15:21:46 +0100
Subject: [PATCH] ressources: use \cat instead of /bin/cat in scripts

---
 ressources/init_repl.sh     | 2 +-
 ressources/launcher_repl.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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