From 0119d04d138bbfcd5db1924eb648cd4cc5aef5b9 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 17 Dec 2023 00:37:18 +0100
Subject: [PATCH] add build script back in

---
 Projects/MathlibLatest/MathlibLatest.lean | 1 -
 Projects/MathlibLatest/lake-manifest.json | 6 ------
 Projects/MathlibLatest/lakefile.lean      | 2 --
 Projects/README.md                        | 3 ---
 server/build.sh                           | 8 ++++++++
 5 files changed, 8 insertions(+), 12 deletions(-)
 create mode 100755 server/build.sh

diff --git a/Projects/MathlibLatest/MathlibLatest.lean b/Projects/MathlibLatest/MathlibLatest.lean
index 5e0851f1..f3335e00 100644
--- a/Projects/MathlibLatest/MathlibLatest.lean
+++ b/Projects/MathlibLatest/MathlibLatest.lean
@@ -1,3 +1,2 @@
 import Mathlib
 import ProofWidgets
-import Webeditor.Tools
diff --git a/Projects/MathlibLatest/lake-manifest.json b/Projects/MathlibLatest/lake-manifest.json
index 3ebd026d..b127db47 100644
--- a/Projects/MathlibLatest/lake-manifest.json
+++ b/Projects/MathlibLatest/lake-manifest.json
@@ -54,12 +54,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"type": "path",
-   "name": "webeditor",
-   "manifestFile": "lake-manifest.json",
-   "inherited": false,
-   "dir": "./../Webeditor",
    "configFile": "lakefile.lean"}],
  "name": "mathlibLatest",
  "lakeDir": ".lake"}
diff --git a/Projects/MathlibLatest/lakefile.lean b/Projects/MathlibLatest/lakefile.lean
index c8ffb680..5d87e806 100644
--- a/Projects/MathlibLatest/lakefile.lean
+++ b/Projects/MathlibLatest/lakefile.lean
@@ -4,8 +4,6 @@ open Lake DSL
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4"@"master"
 
-require webeditor from ".." / "Webeditor"
-
 package mathlibLatest {
   -- add package configuration options here
 }
diff --git a/Projects/README.md b/Projects/README.md
index ccc7b8ae..1797ca07 100644
--- a/Projects/README.md
+++ b/Projects/README.md
@@ -6,8 +6,5 @@ It's important that the project has a file `ProjectName/ProjectName.lean` which
 anything required! Moreover, there should be a file `ProjectName/build.sh` which
 can be called to update the project.
 
-A project would ideally import `import Webeditor from ".." / "Webeditor"` to allow
-the custom lean tools to be available, but that's optional.
-
 You might want to update `Settings.tsx` and add an option to switch to the added
 project.
diff --git a/server/build.sh b/server/build.sh
new file mode 100755
index 00000000..cd85d82f
--- /dev/null
+++ b/server/build.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+SECONDS=0
+
+cd $(dirname $0)
+
+../Projects/Webeditor/build.sh
+../Projects/MathlibLatest/build.sh