Skip to content

Send Feedback using Github issues#3736

Merged
flo2702 merged 1 commit intomainfrom
weigl/ghissue
Mar 16, 2026
Merged

Send Feedback using Github issues#3736
flo2702 merged 1 commit intomainfrom
weigl/ghissue

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Feb 10, 2026

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 current KeYConstant.INTERNAL_VERSION.

Plan

  • Implement it
  • Test it by clicking on it
  • Discussion

Type of pull request

  • New feature (non-breaking change which adds functionality)

Ensuring quality

  • I will made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I have tested the feature as follows: manually clicking the button.

@wadoon wadoon requested a review from mattulbrich February 10, 2026 21:55
@wadoon wadoon self-assigned this Feb 10, 2026
@wadoon wadoon added the GUI label Feb 10, 2026
@wadoon wadoon added this to the v3.0.0 milestone Feb 17, 2026
@wadoon wadoon requested review from flo2702 and removed request for mattulbrich March 14, 2026 13:56
@flo2702 flo2702 added this pull request to the merge queue Mar 16, 2026
Merged via the queue into main with commit d52582d Mar 16, 2026
36 checks passed
@flo2702 flo2702 deleted the weigl/ghissue branch March 16, 2026 15:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants