Skip to content

Improve VSCode support: update developer manual and fix Eclipse nesting errors#1518

Open
HenryXi1 wants to merge 3 commits intoeisop:masterfrom
HenryXi1:update-dev-manual-vscode
Open

Improve VSCode support: update developer manual and fix Eclipse nesting errors#1518
HenryXi1 wants to merge 3 commits intoeisop:masterfrom
HenryXi1:update-dev-manual-vscode

Conversation

@HenryXi1
Copy link

@HenryXi1 HenryXi1 commented Jan 30, 2026

This PR improves support for using VSCode with the Checker Framework.

Changes included:

  1. Update developer manual:

    • Instruct VSCode users to run ./gradlew eclipse instead of ./gradle weclipse classpath.
    • Ensures correct Eclipse project and classpath configuration.
  2. Fix Eclipse nesting errors:

    • Remove bare 'src/main' entries in build.gradle that cause Eclipse to report nesting errors.
    • Ensures source folders are properly recognized and avoids build errors.

@HenryXi1 HenryXi1 changed the title Update developer manual: use ./gradlew eclipse for VSCode Improve VSCode support: update developer manual and fix Eclipse nesting errors Jan 30, 2026
@HenryXi1 HenryXi1 force-pushed the update-dev-manual-vscode branch from fa9c0a3 to 96d0526 Compare January 30, 2026 01:41
@wmdietl
Copy link
Member

wmdietl commented Jan 30, 2026

Thanks for the improvement!

Do you see the CI error messages?
If not, the misc failure is:

+ git diff --exit-code docs/manual/contributors.tex
diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex
index ed211a6a4..83ccd0c90 100644
--- a/docs/manual/contributors.tex
+++ b/docs/manual/contributors.tex
@@ -51,6 +51,7 @@ Haifeng Shi,
 Hamed Taghani,
 Hannes Greule,
 Heath Borders,
+Henry Xi,
 Ivory Wang,
 Jakub Vr\'ana,
 James Yoo,
+ set +x
docs/manual/contributors.tex is not up to date.
If the above suggestion is appropriate, run: make -C docs/manual contributors.tex
If the suggestion contains a username rather than a human name, then do all the following:
  * Update your git configuration by running:  git config --global user.name "YOURFULLNAME"
  * Add your name to your GitHub account profile at https://github.com/settings/profile
  * Make a pull request to add your GitHub ID to
    https://github.com/eisop-plume-lib/git-scripts/blob/master/git-authors.sed
    and remake contributors.tex after that pull request is merged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants