Skip to content

Prevent users from adding tmp to their repository #86

@fingolfin

Description

@fingolfin

... I've seen it more than once.

Solution 1: stop using tmp, instead use mktemp -d to create one (perhaps print the location for the user to aid in debugging). However, IIRC this can complicate things when it comes to building the manual (esp. for packages that rely on the old-style TeX macro based documentation system; for GAPDoc manuals, one needs to worry about links to the GAP manual / other packages. I am not saying these are unsurmountable issues, just that one has to keep them in mind when working on this.

Solution 2: detect if tmp is in the .gitignore file (naive approach: grep for it; better approach: figure out how to ask git whether it consider /tmp/ to be on the ignore list; I am sure there's a way to do that). And if it is not, then issue a warning or even refuse to run.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions