Skip to content

Commit

Permalink
add build script back in
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Dec 16, 2023
1 parent 6a2fa7a commit 0119d04
Show file tree
Hide file tree
Showing 5 changed files with 8 additions and 12 deletions.
1 change: 0 additions & 1 deletion Projects/MathlibLatest/MathlibLatest.lean
Original file line number Diff line number Diff line change
@@ -1,3 +1,2 @@
import Mathlib
import ProofWidgets
import Webeditor.Tools
6 changes: 0 additions & 6 deletions Projects/MathlibLatest/lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -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"}
2 changes: 0 additions & 2 deletions Projects/MathlibLatest/lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
Expand Down
3 changes: 0 additions & 3 deletions Projects/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
8 changes: 8 additions & 0 deletions server/build.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#!/usr/bin/env bash

SECONDS=0

cd $(dirname $0)

../Projects/Webeditor/build.sh
../Projects/MathlibLatest/build.sh

0 comments on commit 0119d04

Please sign in to comment.