use lake serve

joneugster · joneugster · commit 79393d1a5826 · 2025-04-04T01:12:14.000+02:00
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -178,7 +178,7 @@ function App() {
     _leanMonaco.setInfoviewElement(infoviewRef.current!)
     ;(async () => {
         await _leanMonaco.start(options)
-        await leanMonacoEditor.start(editorRef.current!, `/project/${project}.lean`, code)
+        await leanMonacoEditor.start(editorRef.current!, `./${project}.lean`, code)
 
         setEditor(leanMonacoEditor.editor)
         setLeanMonaco(_leanMonaco)
diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh
@@ -33,7 +33,7 @@ if command -v bwrap >/dev/null 2>&1; then
     --unshare-cgroup \
     --die-with-parent \
     --chdir "/project/" \
-    lean --server
+    lake serve --
   )
 else
   echo "bwrap is not installed. Running without container." >&2

Original file line number	Diff line number	Diff line change
`@@ -33,7 +33,7 @@ if command -v bwrap >/dev/null 2>&1; then`
`33`	`33`	`--unshare-cgroup \`
`34`	`34`	`--die-with-parent \`
`35`	`35`	`--chdir "/project/" \`
`36`		`- lean --server`
	`36`	`+ lake serve --`
`37`	`37`	`)`
`38`	`38`	`else`
`39`	`39`	`echo "bwrap is not installed. Running without container." >&2`