From fcb5a56fa7e2021ba99b2040f000bd86231315a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Merlin=20G=C3=B6ttlinger?= Date: Tue, 15 Oct 2019 09:56:56 +0200 Subject: [PATCH] Don't hardcode executable paths `bash` is not specified to reside under `/bin/bash` on all OSs. E.g. on NixOS it does not. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 991d38c1..9f7b534f 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -SHELL := /bin/bash +SHELL := /usr/bin/env bash AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md') AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai') MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))