From bfb437ea36a8c4b83c28b0de79925b447b7d4890 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 22 Nov 2023 08:59:46 +0100 Subject: [PATCH] fix makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c786988..53e6aba 100644 --- a/Makefile +++ b/Makefile @@ -14,7 +14,7 @@ agda: Everything.agda cp Agda.css public/Agda.css clean: - rm -f src/Everything.agda + rm -f Everything.agda rm -rf public/* find . -name '*.agdai' -exec rm \{\} \;