Skip to content

Commit 3974b37

Browse files
committed
use lean --server again
1 parent 4d73cb2 commit 3974b37

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

server/bubblewrap.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ if command -v bwrap >/dev/null 2>&1; then
3333
--unshare-cgroup \
3434
--die-with-parent \
3535
--chdir "/project/" \
36-
lake serve --
36+
lean --server
3737
)
3838
else
3939
echo "bwrap is not installed. Running without container." >&2

server/index.mjs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,19 +30,19 @@ const keyFile = process.env.SSL_KEY_FILE
3030

3131
const app = express()
3232

33-
// `*` has the form `MathlibDemo/MathlibDemo/Logic.lean`
33+
// `*` has the form `mathlib-demo/MathlibLatest/Logic.lean`
3434
app.use('/api/examples/*', (req, res, next) => {
3535
const filename = req.params[0]
3636
req.url = filename
3737
express.static(path.join(__dirname, '..', 'Projects'))(req, res, next)
3838
})
39-
// `*` is the project like `MathlibDemo`
39+
// `*` is the project like `mathlib-demo`
4040
app.use('/api/manifest/*', (req, res, next) => {
4141
const project = req.params[0]
4242
req.url = 'lake-manifest.json'
4343
express.static(path.join(__dirname, '..', 'Projects', project))(req, res, next)
4444
})
45-
// `*` is the project like `MathlibDemo`
45+
// `*` is the project like `mathlib-demo`
4646
app.use('/api/toolchain/*', (req, res, next) => {
4747
const project = req.params[0]
4848
req.url = 'lean-toolchain'

0 commit comments

Comments
 (0)