Skip to content

Comments

Create Config Files for VSCode#83

Merged
andthum merged 6 commits intomainfrom
chore/config-dev-tools
Nov 3, 2022
Merged

Create Config Files for VSCode#83
andthum merged 6 commits intomainfrom
chore/config-dev-tools

Conversation

@andthum
Copy link
Owner

@andthum andthum commented Nov 3, 2022

Create Config Files for VSCode

Type of Change

  • Bug fix.
  • New feature.
  • Code refactoring.
  • Dependency update.
  • Documentation update.
  • Maintenance.
  • Other: Description.
  • Non-breaking (backward-compatible) change.
  • Breaking (non-backward-compatible) change.

Motivation and Context

Support coding with the VSCode/VSCodium code editor.

Proposed Changes

  • Add config files for VSCode.
  • Update existing config files for development.

PR Checklist

  • I followed the guidelines in the Developer's Guide.
  • [~] New/changed code is properly tested.
  • [~] New/changed code is properly documented.
  • [~] New/changed features are tracked in CHANGELOG.rst.
  • The CI workflow is passing.

Add `gmx`, `opthandler` and `strng` to the list of known first-party
libraries.
@github-actions github-actions bot added the maintenance Project maintenance label Nov 3, 2022
Two spaces is the recommended indentation size for the YAML language
(https://www.yaml.info/learn/bestpractices.html).
Exclude VSCode json Config Files from being checked, because VSCode
supports comments in its json config files although this is not allowed
in true json files.
Create a file that contains recommended VSCode extensions for developers
of this workspace (project).  See
https://code.visualstudio.com/docs/editor/extension-marketplace#_workspace-recommended-extensions
Create a config file containing workspace (project) specific settings
for the VSCode editor
(https://code.visualstudio.com/docs/getstarted/settings#_workspace-settings).
@andthum andthum force-pushed the chore/config-dev-tools branch from b7eb970 to 2ba6616 Compare November 3, 2022 10:05
@andthum andthum merged commit 9cd0390 into main Nov 3, 2022
@andthum andthum deleted the chore/config-dev-tools branch November 3, 2022 10:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintenance Project maintenance

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant