diff .hgtags @ 1678:e3de0d89e1c1

use special web.xml when building pdf servlet. building with -ppdf uses web-pdf.xml as web.xml.
author Robert Casties <casties@mpiwg-berlin.mpg.de>
date Wed, 31 Jan 2018 19:55:25 +0100
parents c1e50875a6a3
children
line wrap: on
line diff