React IDE page: add connection and SyncTex alerts (#15273)

Add connection and SyncTex alerts

GitOrigin-RevId: 5004a0d356d0a0355d125516a18db1f57e617a7f
This commit is contained in:
Tim Down
2023-10-19 08:03:04 +00:00
committed by Copybot
parent 3be937c503
commit 87199c80fe
7 changed files with 140 additions and 1 deletions
@@ -9,6 +9,10 @@ block vars
block entrypointVar
- entrypoint = 'pages/ide'
block css
each file in entrypointStyles('ide')
link(rel='stylesheet', href=file)
block content
main#ide-root
.loading-screen