| 1234567891011121314151617 |
- #! /bin/sh
- #
- # Convert a source file to a TeXinfo file. Stolen from glibc.
- #
- # Usage: src2texi SRCDIR SRC TEXI
- dir=$1
- src=`basename $2`
- texi=`basename $3`
- sed -e 's,[{}],@&,g' \
- -e 's,/\*\(@.*\)\*/,\1,g' \
- -e 's,/\* *,/* @r{,g' -e 's, *\*/,} */,' \
- -e 's/\(@[a-z][a-z]*\)@{\([^}]*\)@}/\1{\2}/g' \
- ${dir}/${src} | expand > ${texi}.new
- mv -f ${texi}.new ${dir}/${texi}
|
