diff options
Diffstat (limited to 'tools/release/manuals.pl')
-rwxr-xr-x | tools/release/manuals.pl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/release/manuals.pl b/tools/release/manuals.pl index 3992da53d2..91a67cd684 100755 --- a/tools/release/manuals.pl +++ b/tools/release/manuals.pl | |||
@@ -65,10 +65,10 @@ sub buildit { | |||
65 | `$c`; | 65 | `$c`; |
66 | 66 | ||
67 | print "Run 'make'\n" if($verbose); | 67 | print "Run 'make'\n" if($verbose); |
68 | `make manual 2>/dev/null`; | 68 | `make manual VERSION=$version 2>/dev/null`; |
69 | 69 | ||
70 | print "Run 'make manual-zip'\n" if($verbose); | 70 | print "Run 'make manual-zip'\n" if($verbose); |
71 | `make manual-zip 2>/dev/null`; | 71 | `make manual-zip VERSION=$version 2>/dev/null`; |
72 | } | 72 | } |
73 | 73 | ||
74 | # run make in tools first to make sure they're up-to-date | 74 | # run make in tools first to make sure they're up-to-date |