diff --git a/src/doc_postproc.awk b/src/doc_postproc.awk index de3d3239..b7cb7547 100755 --- a/src/doc_postproc.awk +++ b/src/doc_postproc.awk @@ -78,3 +78,8 @@ BEGIN { { print } + +/