M Fahru
677ec173ed
Disable updating project-wide settings while socket is currently listening to update project-wide settings in a project.
...
This may happen if the project is being used by multiple people, and we want to avoid race condition on the update since it's possible for multiple people to update setting value at the same time.
GitOrigin-RevId: cdad6a6456e2d9e4ef1812ebfd6f6ef59f23747f
2023-01-11 09:08:06 +00:00
M Fahru
af01ace5a0
refactor function by simplifying function argument (from two arguments to a single object)
...
GitOrigin-RevId: e4244a07a4ca196afa226e3fac9de74d30f7d4ea
2023-01-11 09:07:59 +00:00
M Fahru
56395d9a95
Save spellCheckLanguage to both project-wide and user-wide setting
...
GitOrigin-RevId: 059cc64d0fe2e955814a7192f82d4ff8ea4e2572
2023-01-11 09:07:16 +00:00
M Fahru
132bb40a21
replace save project setting hooks with common function and implement set root doc id change
...
GitOrigin-RevId: e5b204cd93fc188288def529cb22018b3d4f89b6
2023-01-11 09:06:40 +00:00
M Fahru
f01a2920cf
Migrate editor settings controller to react (this commit includes project-wide settings)
...
GitOrigin-RevId: 8c47a2699a2f11fda7fd60c5173bf2e29858e37a
2023-01-11 09:05:50 +00:00
