fix stats

leanprover-community · Sep 29, 2024 · 3cdb9a0 · 3cdb9a0
1 parent ebd7268
commit 3cdb9a0
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
@@ -129,8 +129,8 @@ function LandingPage() {
       // Parse the CSV content
       const lines = data.split('\n');
       const [header, line2] = lines;
-      if (!(header.replace(' ', '').startsWith("CPU,Mem"))) {
-        console.warn("unexpected CSV `stats.csv`, expected 'CPU,Mem\\n0.2,0.2\\n', got", header)
+      if (!(header.replace(' ', '').startsWith("CPU,MEM"))) {
+        console.warn("unexpected CSV `stats.csv`, expected 'CPU,MEM\\n0.2,0.2\\n', got", header)
       }
       if (line2) {
         let values = line2.split(',')
@@ -139,6 +139,7 @@ function LandingPage() {
       }
     }).catch(err => {
       console.info('games/stats.csv does not exist')
+      console.info(err)
     })
 
 

diff --git a/doc/server.md b/doc/server.md
@@ -33,7 +33,7 @@ If you would like to display the server capacity on the landing page,
 you can create a file `lean4game/games/stats.csv` of the following form:
 
 ```
-CPU,Mem
+CPU,MEM
 0.1,0.8
 ```