Skip to content
This repository has been archived by the owner on Aug 29, 2023. It is now read-only.

clean up git after leanproject get-mathlib-cache #54

Closed
kckennylau opened this issue Jun 8, 2020 · 5 comments
Closed

clean up git after leanproject get-mathlib-cache #54

kckennylau opened this issue Jun 8, 2020 · 5 comments

Comments

@kckennylau
Copy link
Contributor

Feature request: have leanproject get-mathlib-cache execute at the end:

git reset --hard [commit id specified by leanpkg.toml]
git clean -fd
@gebner
Copy link
Member

gebner commented Jun 8, 2020

I'm very strongly against this change. Most of my mathlib clones have untracked files in them that should not be committed (like bug reports from Zulip, etc.). This change would delete them without warning.

@PatrickMassot
Copy link
Member

PatrickMassot commented Jun 8, 2020

We certainly can't run git clean -fd when editing mathlib itself.

@PatrickMassot
Copy link
Member

I think Kenny wanted to run this inside _target/deps/mathlib, which is currently completely removed when updating.

@kckennylau
Copy link
Contributor Author

yeah this is meant to be for a repo that depends on mathlib, rather than mathlib itself

@PatrickMassot
Copy link
Member

Fixed in b1e6d66

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants