Skip to content

Ignore .git directories when updating a repository #6560

Description

@kit-ty-kate

In some cases (e.g. #6448), a .git directory can make its way into $OPAMROOT/repo/<repo-name>. Currently our internal implementation of diff doesn't do anything clever and will simply diff everything. However this can take a while depending on the hardware and take a significant amount of memory.

We should try to make sure that:

  • every commands do ignore VCS directories
  • the internal diff does ignore it if that repository was already present

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions