Feature: Add collaborative text editing using Yjs, y-webrtc and y-monaco#91

Merged

joneugster merged 22 commits into

leanprover-community:mainfrom

nileshtrivedi:main

May 23, 2026

Commits on Mar 13, 2026

Feature: Add collaborative text editing using Yjs, y-webrtc and y-monaco
nileshtrivedi
committed

Commits on Apr 11, 2026

Commits on Apr 14, 2026

sync with upstream
nileshtrivedi
committed

Commits on Apr 23, 2026

fix: add package-lock.json
joneugster
committed

Commits on May 2, 2026

use env variable to enable/disable feature; write doc; fixes
joneugster
committed

Commits on May 20, 2026

Commits on May 21, 2026

nav bar in mobile layout
joneugster
committed

Commits on May 22, 2026