From c4d825e022fa4aafa8084b37dd46b357827b351b Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 25 Aug 2024 12:10:23 +0200
Subject: [PATCH] cleanup

---
 cypress/e2e/spec.cy.ts  | 5 +++++
 demo/src/LeanMonaco.tsx | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/cypress/e2e/spec.cy.ts b/cypress/e2e/spec.cy.ts
index 3755f8d..5555689 100644
--- a/cypress/e2e/spec.cy.ts
+++ b/cypress/e2e/spec.cy.ts
@@ -10,6 +10,8 @@ describe('Editor Test', () => {
 
   it('displays the infoview', () => {
     cy.on('uncaught:exception', (err, runnable) => {
+      // Note: this is because the server throws sometimes random errors about
+      // the Lean server being stopped/restarted etc. which don't prevent the site from working
       return false
     })
     cy.visit('http://localhost:5173/')
@@ -19,6 +21,7 @@ describe('Editor Test', () => {
 
   it('changes themes', () => {
     cy.on('uncaught:exception', (err, runnable) => {
+      // Note: see note about console errors above
       return false
     })
     cy.visit('http://localhost:5173/')
@@ -38,6 +41,7 @@ describe('Editor Test', () => {
 
   it('inputs unicode', () => {
     cy.on('uncaught:exception', (err, runnable) => {
+      // Note: see note about console errors above
       return false
     })
     cy.visit('http://localhost:5173/')
@@ -53,6 +57,7 @@ describe('Editor Test', () => {
 
   it('allows for multiple editors', () => {
     cy.on('uncaught:exception', (err, runnable) => {
+      // Note: see note about console errors above
       return false
     })
     cy.visit('http://localhost:5173/')
diff --git a/demo/src/LeanMonaco.tsx b/demo/src/LeanMonaco.tsx
index 291578f..ce348c5 100644
--- a/demo/src/LeanMonaco.tsx
+++ b/demo/src/LeanMonaco.tsx
@@ -29,7 +29,7 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti
     <>
       <LeanMonacoContext.Provider value={leanMonaco}>
         {[...Array(numberEditors)].map((_x, i) =>
-          <LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`} value={`#check ${i}\n#eval (panic "oh no" : Nat)`}/>
+          <LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`} value={`#check ${i}`}/>
         )}
         <div className='infoview' ref={infoviewRef}></div>
       </LeanMonacoContext.Provider>