blob: 41ab6fc3566e8fb6adc146908e3739c7be6d009e (
plain)
1
2
3
4
5
6
7
8
9
10
|
#!/bin/bash
set -e
./configure --prefix=/usr &&
makeinfo --html --no-split -o doc/dejagnu.html doc/dejagnu.texi &&
makeinfo --plaintext -o doc/dejagnu.txt doc/dejagnu.texi &&
make -j1 install &&
install -v -dm755 /usr/share/doc/dejagnu-"${VERSION}" &&
install -v -m644 doc/dejagnu.{html,txt} /usr/share/doc/dejagnu-"${VERSION}"
|
