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

Dep: a few tweaks #3651

Merged

mtzguido merged 3 commits into FStarLang:master from mtzguido:deps

Jan 5, 2025

Member

mtzguido commented Jan 5, 2025

Parser.Dep: sort the output to make comparisons of .depends
Parser.Dep: some cleanup and nicer formatting

mtzguido added 3 commits

January 5, 2025 12:59


          Parser.Dep: sort the output to make comparisons of .depends easier

fa58660


          Parser.Dep: some cleanup and nicer formatting

e27cf6c


          snap

a9732ae

mtzguido merged commit e359c3a into FStarLang:master

3 checks passed

mtzguido deleted the deps branch

January 5, 2025 21:52

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

Labels

None yet