echo "make pdf"
make -s pdf
-# And the IDE files\r
-echo "make vc-ide"\r
-make -s vc-ide\r
-\r
+# 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