Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add small section about editing a profile. #6062

Merged
merged 1 commit into from
Feb 24, 2023
Merged

Add small section about editing a profile. #6062

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions docs/editor/profiles.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,12 @@ You can rename an existing profile via the **Rename** command in the Profiles me

You can delete a profile via the **Delete Profile** command. The **Delete Profile** drop down lets you select which profile(s) to delete.

### Edit a profile

To edit a profile no special process is required. You can install/uninstall/disable extensions, change settings and adjust snippets like normale. These changes will be stored in your currently enabled profile.

>**Note**: The `settings.json` file location changes between profiles. Switching profile after opening a `settings.json` will continue to show the previous profiles `settings.json`. Remember to re-open it to see the new settings. This does not apply to the visual settings editor.

### Workspace Associations

When you select create or select an existing profile
Expand Down