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

chore: updates to plugins and dev tools #114

Closed
wants to merge 10 commits into from
Closed

chore: updates to plugins and dev tools #114

wants to merge 10 commits into from

Conversation

sgammon
Copy link
Member

@sgammon sgammon commented Dec 4, 2023

Fixes or Changes Proposed

  • feat: indellij shared indexes
  • chore: wrapper and verification metadata updates
  • chore: ignore project indexes
  • chore: add buildless github action

@sgammon sgammon added the dependencies Tasks and PRs dealing with dependencies label Dec 4, 2023
@sgammon sgammon self-assigned this Dec 4, 2023
@github-actions github-actions bot removed the dependencies Tasks and PRs dealing with dependencies label Dec 4, 2023
@sgammon sgammon changed the title Chore/updates chore: updates to plugins and dev tools Dec 4, 2023
@sgammon sgammon marked this pull request as ready for review December 4, 2023 08:20
@sgammon sgammon closed this Jan 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@sgammon sgammon

Labels
None yet
Projects
Elide
Status: Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@sgammon