Skip to content
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.

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

Makefile: fix clean rule #3535

Merged
merged 1 commit into from
Oct 7, 2024
Merged

Makefile: fix clean rule #3535

merged 1 commit into from
Oct 7, 2024

Conversation

mtzguido
Copy link
Member

@mtzguido mtzguido commented Oct 7, 2024

The clean-buildfiles subrule could only work after a build, and failed on a fresh repo. Given we only needed it to decrease the size of docker images after a build (which we soon won't do) and didn't have automatic pruning (we do now), this is not that useful.

Just remove it and clean as before.


@tahina-pro I broke this and didn't notice, sorry. I think this doesn't really matter now since we autoclean the docker images (and that will all be gone with new CI soon).

The clean-buildfiles subrule could only work after a build, and failed
on a fresh repo. Given we only needed it to decrease the size of docker
images after a build (which we soon won't do) and didn't have automatic
pruning (we do now), this is not that useful.

Just remove it and clean as before.
@mtzguido mtzguido merged commit 4962891 into FStarLang:master Oct 7, 2024
2 checks passed
@mtzguido mtzguido deleted the clean branch October 7, 2024 16:53
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.

1 participant