Skip to content

Update configuration of development tools#144

Merged
andthum merged 8 commits intomainfrom
chore/config
Feb 13, 2023
Merged

Update configuration of development tools#144
andthum merged 8 commits intomainfrom
chore/config

Conversation

@andthum
Copy link
Owner

@andthum andthum commented Feb 13, 2023

Update configuration of development tools

Type of change

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

PR checklist

  • I followed the guidelines in the Developer's guide.
  • [~] New/changed code is properly tested.
  • [~] New/changed code is properly documented.
  • The CI workflow is passing.

@github-actions github-actions bot added the maintenance Project maintenance label Feb 13, 2023
@andthum andthum merged commit 25ef016 into main Feb 13, 2023
@andthum andthum deleted the chore/config branch February 13, 2023 09:23
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