diff options
| author | Peter Eisentraut | 2018-02-28 13:22:51 +0000 |
|---|---|---|
| committer | Peter Eisentraut | 2018-03-08 18:32:10 +0000 |
| commit | 353dd75260e00379240be6a7b8897e90449a95db (patch) | |
| tree | 0af19f454e69683c860a21568ec8014f762bff82 /src | |
| parent | d4429d50a21adcc0543701350d5112e3868a3596 (diff) | |
Fix warnings in man page build
The changes in the CREATE POLICY man page from commit
87c2a17fee784c7e1004ba3d3c5d8147da676783 triggered a stylesheet bug that
created some warning messages and incorrect output. This installs a
workaround.
Also improve the whitespace a bit so it looks better.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions