repo.or.cz
/
dejagnu.git
/
blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
log
|
graphiclog1
|
graphiclog2
|
commit
|
commitdiff
|
tree
|
refs
|
edit
|
fork
blame
|
history
|
raw
|
HEAD
* deb: Move from here ..
[dejagnu.git]
/
packaging
/
deb
/
postinst
blob
12a4ea564824bce34b13e4820a22d8d440bd0f6b
1
#! /bin/sh
2
3
set -i
4
5
#install-info --quiet --section "Development" "Development" \
6
#/usr/doc/dejagnu.info.gz
7
8
echo
"Edit the master configuration file, /etc/dejagnu/site.exp, if needed"