info-postASP.awk: make sure ref names are sanitized as other node names

parent 702c78e4
......@@ -132,7 +132,7 @@ END {
{
}
else if ( $1=="@REF" ) {
print "@ref{" labels[$2] "}";
print "@ref{" cleannodename(labels[$2]) "}";
}
else if ( $1=="@SUB" ) {
if ( firstsec==1 ) {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment