Fix Makefile.
This commit is contained in:
parent
bfc0b7f598
commit
56613e9d5e
1 changed files with 5 additions and 2 deletions
7
Makefile
7
Makefile
|
@ -1,6 +1,6 @@
|
|||
SHELL := /usr/bin/env bash
|
||||
AGDA_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
|
||||
AGDAI_FILES := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
|
||||
AGDA_FILES := $(shell find . -type f -and \( -path './src/*' -or -path './courses/*' \) -and -name '*.lagda.md')
|
||||
AGDAI_FILES := $(shell find . -type f -and \( -path './src/*' -or -path './courses/*' \) -and -name '*.agdai')
|
||||
MARKDOWN_FILES := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA_FILES))))
|
||||
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
||||
PANDOC := pandoc
|
||||
|
@ -27,6 +27,9 @@ else
|
|||
SEDI := sed -i
|
||||
endif
|
||||
|
||||
bla:
|
||||
@echo $(AGDA_FILES)
|
||||
|
||||
|
||||
# Build PLFA web version and test links
|
||||
default: test
|
||||
|
|
Loading…
Reference in a new issue