Skip to content

Commit

Permalink
reinsert vscode.css
Browse files Browse the repository at this point in the history
Fixes #15
  • Loading branch information
abentkamp committed Dec 8, 2023
1 parent 0b1d361 commit e988cba
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions client/src/Editor.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ import * as React from 'react'
import { useEffect, useRef, useState } from 'react'
import './css/Editor.css'
import './editor/infoview.css'
import './editor/vscode.css'
import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { loadRenderInfoview } from '@leanprover/infoview/loader'
import { InfoviewApi } from '@leanprover/infoview-api'
Expand Down

0 comments on commit e988cba

Please sign in to comment.