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