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: Minor Dotty tweak #2946

Merged

tippmar-nr merged 2 commits into main from chore/dotty-tweak

Jan 13, 2025

Member

tippmar-nr commented Jan 13, 2025 •

edited

Loading

Minor tweaks to Dotty, mostly about adding a reminder to update the compatibility docs in the body of the PR.
Removed some unused variables.
Added a workflow to build the BuildTools solution when relevant files are modified.


          chore: Minor Dotty tweak

6e267d0

tippmar-nr requested a review from a team as a code owner

January 13, 2025 21:45

tippmar-nr enabled auto-merge (squash)

January 13, 2025 21:45


          Add workflow to build buildtools.sln

f70c28e

chynesNR approved these changes

View reviewed changes

tippmar-nr merged commit 655b872 into main

18 checks passed

tippmar-nr deleted the chore/dotty-tweak branch

January 13, 2025 22:41

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

Labels

None yet