Send Feedback using Github issues #3736
Open
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Intended Change
This PR adds a new menu item to create issues on GitHub directly from this repository.
This functionality uses the Github URL API; no API key is required, and the user's account is used. (It just prefills the issues form.)
Note: the length of URLs is limited.
It automatically inserts all Java files findable in the current
JavaModel#modelDir, and the currentKeYConstant.INTERNAL_VERSION.Plan
Type of pull request
Ensuring quality