diff options
-rwxr-xr-x | maketgz | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -125,8 +125,8 @@ make -s pdf # And the IDE files
echo "make vc-ide"
-make -s vc-ide
-
+make -s vc-ide + echo "produce CHANGES" git log --pretty=fuller --no-color --date=short --decorate=full -1000 | ./log2changes.pl > CHANGES.dist |