Skip to content

Commit

Permalink
Merge PR coq#19919: Remove generated dune files on "make clean"
Browse files Browse the repository at this point in the history
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>
  • Loading branch information
coqbot-app[bot] and SkySkimmer authored Dec 17, 2024
2 parents 44e65b6 + 2746813 commit ccd5d96
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ ireport:
dune build $(DUNEOPT) @install --profile=ireport

clean:
rm -f .dune-stamp
rm -f .dune-stamp theories/dune user-contrib/Ltac2/dune
dune clean

# docgram
Expand Down

0 comments on commit ccd5d96

Please sign in to comment.