Fixed make: Nothing to be done for `clean'.
This commit is contained in:
parent
ebbd1604b6
commit
ecc468c84d
1 changed files with 1 additions and 1 deletions
2
Makefile
2
Makefile
|
@ -1,5 +1,5 @@
|
||||||
agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda)
|
agda := $(wildcard src/*.lagda) $(wildcard src/**/*.lagda)
|
||||||
agdai := $(patsubst %.lagda,%.agdai,$(agda))
|
agdai := $(wildcard src/*.agdai) $(wildcard src/**/*.agdai)
|
||||||
markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
|
markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
|
||||||
|
|
||||||
all: bugfix $(markdown)
|
all: bugfix $(markdown)
|
||||||
|
|
Loading…
Reference in a new issue