From 080b46329e75e17248bc4a68c8cd7856ae5b950e Mon Sep 17 00:00:00 2001 From: Kevin Veen-Birkenbach Date: Tue, 1 Apr 2025 21:19:05 +0200 Subject: [PATCH] Removed unneccessary MAkefile --- Makefile | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 Makefile diff --git a/Makefile b/Makefile deleted file mode 100644 index 6f0489fd..00000000 --- a/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -.PHONY: install deinstall refresh - -install: - $(MAKE) -C docs html $(MAKEFLAGS) - $(MAKE) -C docs install $(MAKEFLAGS) - -deinstall: - $(MAKE) -C docs clean $(MAKEFLAGS) - -refresh: - $(MAKE) -C docs clean $(MAKEFLAGS) - $(MAKE) -C docs html $(MAKEFLAGS)