grrr, missed them in my previous fix
@@ -123,8 +123,8 @@ make -s html
echo "make pdf"
make -s pdf
# And the IDE files
echo "make vc-ide"
make -s vc-ide
echo "produce CHANGES"
The note is not visible to the blocked user.