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.

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

Add clean in Makefile #120

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add clean in Makefile #120

wants to merge 1 commit into from

Conversation

Villetaneuse
Copy link
Contributor

Also make dune, all, install and dune-install .PHONY

Fixes / closes #????

@Villetaneuse
Add clean in Makefile
01ebc88 
Also make `dune`, `all`, `install` and `dune-install` .PHONY
@proux01
Copy link
Contributor

proux01 commented Mar 11, 2025

I usually prefer to use git clean than any make clean target that are likely to be broken or incomplete.
But if you find any use to it, fine by me.

@proux01 proux01 added this to the 9.0 milestone Mar 11, 2025
@Villetaneuse
Copy link
Contributor Author

Well I could have some uncommited files that I want to preserve; while still wanting to recompile everything to check if there are warnings. Anyway, it probably does not harm.

@proux01
Copy link
Contributor

proux01 commented Mar 11, 2025

Well I could have some uncommited files that I want to preserve

In that case, I prefer to git add the file, and potentially keep it in a temporary branch.

Anyway, it probably does not harm.

Sure, go ahead

SkySkimmer
SkySkimmer reviewed Mar 11, 2025
View reviewed changes
Makefile
-o -name '*.vok' \
-o -name '*.vos' \
-o -name '*.glob' \
-exec rm -vf {} +
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

seems incomplete
at least missing the .d and the coq-native files
you could call rocq makefile's make clean if the Makefile.coq exists
also you could rm -rf _build

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you. Didn't know about these. Can you give me a pointer to these .d and coq-native files?

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

@SkySkimmer SkySkimmer SkySkimmer left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
9.0
Development

Successfully merging this pull request may close these issues.
3 participants
@Villetaneuse @proux01 @SkySkimmer