phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

add logic game to landing page

Browse Source
This commit is contained in:
Jon Eugster
2024-01-22 13:31:43 +01:00
parent e085f2f106
commit 36bc52c960
2 changed files with 4 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/landing_page.tsx
+2 -1
View File
@@ -134,7 +134,8 @@ function LandingPage() {
"leanprover-community/nng4", "leanprover-community/nng4",
"hhu-adam/robo", "hhu-adam/robo",
"djvelleman/stg4", "djvelleman/stg4",
"miguelmarco/STG4", "miguelmarco/stg4",
"trequetrum/lean4game-logic",
] ]
let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
relay/index.mjs
+2 -1
View File
@@ -19,7 +19,8 @@ import { importTrigger, importStatus } from './import.mjs'
const queueLength = { const queueLength = {
"g/hhu-adam/robo": 2, "g/hhu-adam/robo": 2,
"g/hhu-adam/nng4": 5, "g/hhu-adam/nng4": 5,
"g/djvelleman/stg4": 2, "g/djvelleman/stg4": 0,
"g/trequetrum/lean4game-logic": 0,
} }
const __filename = url.fileURLToPath(import.meta.url); const __filename = url.fileURLToPath(import.meta.url);