codespace
codespace copied to clipboard
Persists user's own `rstudio-prefs.json`
@rongxin-liu, what do you think is best here? I'm currently persisting user prefs to (1), but would (2) or (3) perhaps be best?
/workspaces/$RepositoryName/rstudio-prefs.json, in which case it appears in file explorer/workspaces/$RepositoryName/.config/rstudio/rstudio-prefs.json, similar to where it ends up inrstudiocontainer, but won't be backed up (at the moment) via GitDoc, since it'd be in a dotfolder/home/ubuntu/.config/rstudio/rstudio-prefs.json, more similar to where it ends up inrstudiocontainer, but it wouldn't persist after rebuilds either- other...
When people take the CS50R course, they rarely need to update (rebuild) their Codespace (because running rstudio ensures they get the latest RStduio so they don't really need the latest Codespace version), so options 2 and 3 are fine. It wouldn't be much hassle for people to re-customize their R studio after a codespace rebuild.
Agreed with @rongxin-liu!