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.

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

chore: VS Code settings #768

Merged
merged 4 commits into from
Feb 19, 2025
Merged

chore: VS Code settings #768

merged 4 commits into from
Feb 19, 2025

Conversation

Jinxit
Copy link
Contributor

@Jinxit Jinxit commented Feb 19, 2025

Description

Decided to split this from CI changes to make it an easier thing to get merged. There are now two main changes:

  1. RA uses a separate target directory, meaning RA builds no longer cause rebuilds in nix, and vice versa.
  2. The settings file has been renamed to settings.default.json, meaning developers can copy that file as a starting point but have their own settings that won't be committed to the repo.

Important points for reviewers

If you don't make a copy of settings.default.json as settings.json after this is merged, you won't have the right settings in VS Code.

Checklist

  • Are there important points that reviewers should know?
    • See above.
  • Make sure that you described what this change does.
  • If there are follow-ups, have you created issues for them?
  • Have you tested this solution?
  • Were there any alternative implementations considered?
  • Did you document new (or modified) APIs?

@Jinxit Jinxit added the ready for review Review is needed label Feb 19, 2025
@Jinxit Jinxit enabled auto-merge (squash) February 19, 2025 16:05
Copy link
Collaborator

@jmg-duarte jmg-duarte left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. I wonder if there's a way to tell git "dont actually delete settings.json locally, just remove from cache"

@Jinxit Jinxit merged commit c13c0ad into develop Feb 19, 2025
6 checks passed
@Jinxit Jinxit deleted the chore/dev-ex branch February 19, 2025 17:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready for review Review is needed
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants