diff options
Diffstat (limited to 'scripts/hxtool')
| -rw-r--r-- | scripts/hxtool | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scripts/hxtool b/scripts/hxtool index 7ca83ed1ff..995bb7f08c 100644 --- a/scripts/hxtool +++ b/scripts/hxtool @@ -47,6 +47,9 @@ hxtotexi() DEFHEADING*) echo "$(expr "$str" : "DEFHEADING(\(.*\))")" ;; + ARCHHEADING*) + echo "$(expr "$str" : "ARCHHEADING(\(.*\),.*)")" + ;; *) test $flag -eq 1 && echo "$str" ;; |