From e86a460eb98adfaf4a9b4645615e9cc9f209ad2c Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 15 May 2023 15:05:53 +0200
Subject: [PATCH] remove deprecated UPDATE_LEAN.sh

---
 UPDATE_LEAN.sh | 19 -------------------
 1 file changed, 19 deletions(-)
 delete mode 100644 UPDATE_LEAN.sh

diff --git a/UPDATE_LEAN.sh b/UPDATE_LEAN.sh
deleted file mode 100644
index 27ebc35..0000000
--- a/UPDATE_LEAN.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/env sh
-
-# Operate in the directory where this file is located
-cd $(dirname $0)
-
-cd server
-
-cd adam
-lake update
-
-cp lake-packages/mathlib/lean-toolchain lean-toolchain
-cp lake-packages/mathlib/lean-toolchain ../lean-toolchain
-cp lake-packages/mathlib/lean-toolchain ../nng/lean-toolchain
-
-cd ../
-lake update
-
-cd ../nng
-lake update