@@ -125,8 +125,8 @@ make -s pdf
# And the IDE files
echo "make vc-ide"
make -s vc-ide
echo "produce CHANGES"
git log --pretty=fuller --no-color --date=short --decorate=full -1000 | ./log2changes.pl > CHANGES.dist
The note is not visible to the blocked user.