Getting rid of bash-style <<< redirection, using general | instead.

stepcut · Nov 12, 2020 · 6c85dee · 6c85dee
1 parent a61b977
commit 6c85dee
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/aux-makefiles/Idris2.mk b/aux-makefiles/Idris2.mk
@@ -19,12 +19,12 @@ OTHER_OBJS += $(RTS_OBJS)
 include $(ARDUINO_MAKEFILE_PATH)
 
 ifdef BOSSA_OPTS
-  BOSSA_OPTS != sed "s/-d //" <<< "$(BOSSA_OPTS)"
+  BOSSA_OPTS != echo "$(BOSSA_OPTS)" | sed "s/-d //"
 endif
 
 build/exec/%.c: %.idr
 	rm -f "$@"
-	CC=true idris2 --codegen refc "$<" <<< ":compile $(basename $(notdir "$@")) main"
+	echo ":compile $(basename $(notdir "$@")) main" | CC=true idris2 --codegen refc "$<"
 	sed -i 's/Value \*mainExprVal/init();\n   Value *mainExprVal/' "$@"
 	sed -i 's|// add header(s) for library: libarduino|#include "Arduino.h"|' "$@"