jenkins.sh: disable 'publish' of manuals; we don't have any yet

Change-Id: Ib5fb783e4e7e5e327e474344220206f33c64a8bd
1 file changed