diff options
author | Eelco Dolstra <e.dolstra@tudelft.nl> | 2003-08-22T20·12+0000 |
---|---|---|
committer | Eelco Dolstra <e.dolstra@tudelft.nl> | 2003-08-22T20·12+0000 |
commit | a88144215c263e62528108dfae1e781058344ef2 (patch) | |
tree | ff44455c3a5a5d4e6b3a556c78cc1511f7630378 /src/util.hh | |
parent | 56b98c3857b89d4f81f0127c53cfce6d8e48a71f (diff) |
* Remove write permission from output paths after they have been built.
* Point $HOME to a non-existing path when building to prevent certain tools (such as wget) from falling back on /etc/passwd to locate the home directory (which we don't want them to look at since it's not declared as an input).
Diffstat (limited to 'src/util.hh')
-rw-r--r-- | src/util.hh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/util.hh b/src/util.hh index 2863085c16f9..d0e42f3b1707 100644 --- a/src/util.hh +++ b/src/util.hh @@ -67,7 +67,10 @@ bool pathExists(const string & path); /* Delete a path; i.e., in the case of a directory, it is deleted recursively. Don't use this at home, kids. */ -void deletePath(string path); +void deletePath(const string & path); + +/* Make a path read-only recursively. */ +void makePathReadOnly(const string & path); /* Messages. */ |