Skip to content

Commit

Permalink
bump; part 3
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Mar 5, 2025
1 parent deaab6a commit 41f1e24
Show file tree
Hide file tree
Showing 5 changed files with 14 additions and 9 deletions.
4 changes: 2 additions & 2 deletions Projects/mathlib-demo/lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "a3eb54483cfad2b312c98f5b88d3386e58b2628c",
"rev": "a69bc35b7028de551fb3c101d72f5ddbef2a6b2d",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand Down Expand Up @@ -75,7 +75,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
"rev": "b8e143008dc1e5f28f48a8aa8de63deaf4fe8068",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
2 changes: 1 addition & 1 deletion client/src/Navigation.tsx
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import { ChangeEvent, Dispatch, FC, MouseEventHandler, ReactNode, SetStateAction, useContext, useState } from 'react'
import { ChangeEvent, Dispatch, FC, JSX, MouseEventHandler, ReactNode, SetStateAction, useContext, useState } from 'react'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { IconDefinition, faArrowRotateRight, faCode, faInfoCircle } from '@fortawesome/free-solid-svg-icons'
import ZulipIcon from './assets/zulip.svg'
Expand Down
2 changes: 2 additions & 0 deletions client/src/config/docs.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
* This file contains the documentation of the existing `config` options
*/

import { JSX } from "react"

/** An example can be any Lean file which belongs to the project.
* The editor just reads the file content, but it makes sense for maintainability
* that you ensure the Lean project actually builds the file. */
Expand Down
8 changes: 4 additions & 4 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 5 additions & 2 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,10 @@
"bin": {
"server": "server/index.mjs"
},
"files": ["client/dist", "server"],
"files": [
"client/dist",
"server"
],
"scripts": {
"start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"",
"start_server": "cd server && NODE_ENV=development nodemon ./index.mjs",
Expand Down Expand Up @@ -46,7 +49,7 @@
"ws": "^8.18.1"
},
"devDependencies": {
"@codingame/esbuild-import-meta-url-plugin": "https://gitpkg.vercel.app/abentkamp/monacotest2/esbuild-import-meta-url-plugin?ec9666e",
"@codingame/esbuild-import-meta-url-plugin": "^1.0.3",
"@types/node": "^22.13.9",
"@types/react": "^19.0.10",
"@types/react-dom": "^19.0.4",
Expand Down

0 comments on commit 41f1e24

Please sign in to comment.