diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-11 15:28:02 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-11 15:28:02 +0200 |
| commit | 0df003671aa3c607977272571d89a4f6bad1c1e9 (patch) | |
| tree | 69ade9100ddb36271c7a9fe4bc84d0ce456790e8 /Makefile | |
| parent | f3c60be7e370b20cccbb006d3cba907e15659656 (diff) | |
| download | compcert-0df003671aa3c607977272571d89a4f6bad1c1e9.tar.gz compcert-0df003671aa3c607977272571d89a4f6bad1c1e9.zip | |
Makefile: chmod a-w instead of chmod -w
The latter, in conjunction with some values of the umask, gives weird messages
"new permissions are ... not ...".
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -207,7 +207,7 @@ latexdoc: @rm -f $*.v @echo "Preprocessing $*.vp" @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } - @chmod -w $*.v + @chmod a-w $*.v compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ |