mirror of
https://git.savannah.gnu.org/git/grub.git
synced 2026-10-22 15:22:39 +00:00
Robert Millan
f4a573f875
Use more standard `doc' directory. * docs: Rename to ... * doc: ... this. Update all users. * doc/multiboot.texi: Fix an obsolete reference to `docs' directory in GRUB distribution.
17 lines
395 B
Bash
17 lines
395 B
Bash
#! /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}
|