aboutsummaryrefslogtreecommitdiff
path: root/scripts/hxtool
diff options
context:
space:
mode:
Diffstat (limited to 'scripts/hxtool')
-rw-r--r--scripts/hxtool11
1 files changed, 9 insertions, 2 deletions
diff --git a/scripts/hxtool b/scripts/hxtool
index 04f7d7b0ed..5468cd7782 100644
--- a/scripts/hxtool
+++ b/scripts/hxtool
@@ -16,6 +16,13 @@ hxtoh()
done
}
+print_texi_heading()
+{
+ if test "$*" != ""; then
+ printf "@subsection %s\n" "$*"
+ fi
+}
+
hxtotexi()
{
flag=0
@@ -45,10 +52,10 @@ hxtotexi()
fi
;;
DEFHEADING*)
- printf '%s\n' "$(expr "$str" : "DEFHEADING(\(.*\))")"
+ print_texi_heading "$(expr "$str" : "DEFHEADING(\(.*\))")"
;;
ARCHHEADING*)
- printf '%s\n' "$(expr "$str" : "ARCHHEADING(\(.*\),.*)")"
+ print_texi_heading "$(expr "$str" : "ARCHHEADING(\(.*\),.*)")"
;;
*)
test $flag -eq 1 && printf '%s\n' "$str"