diff --git a/client/src/index.tsx b/client/src/index.tsx
index 2b593c6..85c6c83 100644
--- a/client/src/index.tsx
+++ b/client/src/index.tsx
@@ -1,29 +1,45 @@
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
+import * as React from 'react'
+import { createRoot } from 'react-dom/client'
+import App from './app'
import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
- createHashRouter,
- RouterProvider,
- Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
+import { store } from './state/store'
+import { Provider } from 'react-redux'
+import type { RouteObject } from "react-router"
+import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
+import ErrorPage from './components/error_page'
+import Welcome from './components/welcome'
+import LandingPage from './components/landing_page'
+import Level from './components/level'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+
monacoSetup()
+// // Do not show the landing page in the dev-container context
+// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? {
+// path: "/",
+// loader: () => redirect("/g/local/game")
+// } : {
+// path: "/",
+// element: ,
+// }
+
+
+// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
+// `/g/local/game`. This is used for the devcontainer setup
+let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
+let root_object: RouteObject = single_game ? {
+ path: "/",
+ loader: () => redirect("/g/local/game")
+} : {
+ path: "/",
+ element: ,
+}
+
const router = createHashRouter([
+ root_object,
{
- path: "/",
- element: ,
- },
- {
+ // For backwards compatibility
path: "/game/nng",
loader: () => redirect("/g/hhu-adam/NNG4")
},
diff --git a/client/src/index_local.tsx b/client/src/index_local.tsx
deleted file mode 100644
index 9328768..0000000
--- a/client/src/index_local.tsx
+++ /dev/null
@@ -1,55 +0,0 @@
-// This file is a copy of `index.tsx` where the path "/" is redirected to "/g/local/game".
-// It is used for the dev. setup where there is only one game in a folder called `game`.
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
-import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
- createHashRouter,
- RouterProvider,
- Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
-
-monacoSetup()
-
-const router = createHashRouter([
- {
- path: "/",
- loader: () => redirect("/g/local/game")
- },
- {
- path: "/g/:owner/:repo",
- element: ,
- errorElement: ,
- children: [
- {
- path: "/g/:owner/:repo",
- element: ,
- },
- {
- path: "/g/:owner/:repo/world/:worldId/level/:levelId",
- element: ,
- },
- ],
- },
-]);
-
-const container = document.getElementById('root');
-const root = createRoot(container!);
-root.render(
-
-
-
-
-
-
-
-);
diff --git a/env.d.ts b/env.d.ts
new file mode 100644
index 0000000..4d10cb9
--- /dev/null
+++ b/env.d.ts
@@ -0,0 +1,10 @@
+///
+
+interface ImportMetaEnv {
+ readonly VITE_LEAN4GAME_SINGLE: string
+ // more env variables...
+}
+
+interface ImportMeta {
+ readonly env: ImportMetaEnv
+}