From 08046d05dcddc3a8e14083142a09c0c79edba46c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 29 May 2018 15:35:20 +0200 Subject: [PATCH] Update makefile --- Makefile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index bec101b..6f8e63d 100644 --- a/Makefile +++ b/Makefile @@ -4,8 +4,10 @@ build: src/**.agda clean: find src -name "*.agdai" -type f -delete -html: +html: src/**.agda agda --html src/Cat.agda upload: html scp -r html/ remote11.chalmers.se:www/cat/doc/ + +.PHONY: upload clean