gap-system/ReleaseTools

Prevent users from adding `tmp` to their repository

fingolfin opened this issue · 0 comments

... 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.