Fix bug with find on DICE

This commit is contained in:
Wen Kokke 2019-01-08 09:40:44 +00:00
parent 4a80d4e0e3
commit 61163eb056

View file

@ -1,5 +1,5 @@
agda := $(shell find src tspl -type f -name '*.lagda')
agdai := $(shell find src tspl -type f -name '*.agdai')
agda := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.lagda')
agdai := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.agdai')
markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
@ -84,6 +84,13 @@ clobber: clean
.phony: clobber
# List all .lagda files
ls:
@echo $(agda)
.phony: ls
# MacOS Setup (install Bundler)
macos-setup:
brew install libxml2