-prevent editing of generated files

This commit is contained in:
Christian Grothoff 2022-06-13 09:47:25 +02:00
parent 7876bc0600
commit 007cc7abe8
No known key found for this signature in database
GPG Key ID: 939E6BE1E29FC3CC

View File

@ -23,6 +23,7 @@ ensure ()
if ! diff $src/$fn $dst/$fn > /dev/null if ! diff $src/$fn $dst/$fn > /dev/null
then then
cp $src/$fn $dst/$fn cp $src/$fn $dst/$fn
chmod -w $dst/$fn
fi fi
} }