diff options
| author | Peter Eisentraut <peter_e@gmx.net> | 2018-02-28 08:22:51 -0500 |
|---|---|---|
| committer | Peter Eisentraut <peter_e@gmx.net> | 2018-03-08 13:31:57 -0500 |
| commit | 2f09dc11936b8656328ad66f7dc7d2dd5e45ed9e (patch) | |
| tree | a89a62cfb2e9a3b82e1267339e9eeb3296c4bdcf /src | |
| parent | 8e5c2afa98d9c28c9883c4c42890f3a6dd99ba4e (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