diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2018-10-09 16:04:39 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2018-10-09 22:56:17 -0400 |
| commit | 32112efcb3522acbece4515b849d40973e48c973 (patch) | |
| tree | a88d388e001d723d263053c6bb60b49c66cffc7c /src/Util | |
| parent | 0842563b23f8d780f4ff1080d7620fc3f368191f (diff) | |
Remove [Redirect] to absolute paths
find . -name '*.v' -print0 | xargs -0 sed -i 's/^\(\s*\)\(Redirect.*\.\)$/\1(* \2 *)/g'
When on a shared machine, the first user would create /tmp/outfile and
then the build would fail for the second user because the file already
exists and is owned by somebody else.
https://github.com/coq/coq/issues/8649
tested ok on top of c4e09295f5a8e10ea1957711da0e79661177e8a6
Diffstat (limited to 'src/Util')
0 files changed, 0 insertions, 0 deletions