From c6212ccb8b650224e51907da3b4db0d52ca9f2a6 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 16 Aug 2024 09:42:19 +1000
Subject: [PATCH] chore: remove makefile

---
 GNUmakefile | 12 ------------
 README.md   |  4 +++-
 2 files changed, 3 insertions(+), 13 deletions(-)
 delete mode 100644 GNUmakefile

diff --git a/GNUmakefile b/GNUmakefile
deleted file mode 100644
index 123c8af1a1..0000000000
--- a/GNUmakefile
+++ /dev/null
@@ -1,12 +0,0 @@
-.PHONY: all build test lint
-
-all: build test
-
-build:
-	lake build
-
-test:
-	lake test
-
-lint:
-	lake exe runLinter
diff --git a/README.md b/README.md
index f5f241fe22..ab8606d854 100644
--- a/README.md
+++ b/README.md
@@ -23,7 +23,9 @@ Additionally, please make sure that you're using the version of Lean that the cu
   curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
   ```
   If this also fails, follow the instructions under `Regular install` [here](https://leanprover-community.github.io/get_started.html).
-* To build `batteries` run `lake build`. To build and run all tests, run `make`.
+* To build `batteries` run `lake build`.
+* To build and run all tests, run `lake test`.
+* To run the environment linter, run `lake lint`.
 * If you added a new file, run the command `scripts/updateBatteries.sh` to update the
   imports.