/usr/share/debci/bin/debci-config is in debci 1.0.2.
This file is owned by root:root, with mode 0o755.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 | #!/bin/sh
set -eu
usage() {
echo "Usage: debci config [OPTIONS] KEY [KEY ..]"
echo
echo "Display the values for the passed KEYs"
if [ $# -ne 0 ]; then
echo
echo "$@"
fi
}
debci_base_dir=$(readlink -f $(dirname $(readlink -f $0))/..)
cd $debci_base_dir
. lib/environment.sh
prepare_args
if [ $# -eq 0 ]; then
usage
exit 1
fi
notfound=0
for key in "$@"; do
eval "value=\"\${debci_${key}:-}\""
eval "set=\"\${debci_${key}+set}\""
if [ -n "$set" ]; then\
echo "$key=$value"
else
echo "E: key $key not found!" >&2
notfound=$(expr $notfound + 1)
fi
done
exit $notfound
|