docs/tools/xml_insert: fix awk warning

diff --git a/docs/tools/xml_insert.sh b/docs/tools/xml_insert.sh
index 16b6b246d69e4f3a0d0416261f81c421f6844b44..7d8bf686e3e70c0dab85834a9e2f577dfddd479c 100755 (executable)
--- a/docs/tools/xml_insert.sh
+++ b/docs/tools/xml_insert.sh
@@ -91,7 +91,7 @@ tmp_file="$tmp_dir/one"
 cp $1 $tmp_file
 
 numlines=`wc -l $tmp_file | $AWK '{print $1;}'`
-splitno=`$AWK "/<\!--$2-->/ { print NR; exit 0; }" $tmp_file`
+splitno=`$AWK "/<!--$2-->/ { print NR; exit 0; }" $tmp_file`
 tailno=`expr $numlines - $splitno`
 
 head -$splitno $tmp_file > $1