Merge pull request #14319 from grahamc/jenkins
jenkins: copy .war to $out, fixes #14137
Domen Kožar 10 years ago 253af9a0 16969218