From 6c85dee0d5854554525086bff2139cf8a34e79e0 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Thu, 12 Nov 2020 17:22:52 +0300 Subject: [PATCH] Getting rid of bash-style `<<<` redirection, using general `|` instead. --- aux-makefiles/Idris2.mk | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/aux-makefiles/Idris2.mk b/aux-makefiles/Idris2.mk index 0dc21cb..c15e606 100644 --- 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"|' "$@"