Skip to content

dune cache clear does not clear the toolchains cache #11585

@emillon

Description

@emillon

Hi,
With the default configuration, dune cache clear leaves ~/.cache/dune/toolchains in place.

I understand the technical reason, but it's a bit confusing. I think that the goal of dune cache clear is to replace rm -r ~/.cache/dune but it's now necessary again.

If removing the toolchains cache by default is not desirable, maybe an extra flag to remove this cache would work.

(noting the caveat in #11584 that these might not be in the same location)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions