#!/bin/bash
#  exec - Command execution support library

set -e


run() {
	info "Running $@ ..."
	if $pretend; then
		return
	fi
	local cmd=$1
	shift
	if type "$cmd" >/dev/null 2>&1; then
		$cmd "$@"
	else
		debug=true
		error "$cmd: unknown command"
	fi
}
run_sudo() { run sudo -H -- "$@"; }
run_sudo_as_user() {
        local user=$1
        shift
        run sudo -u $user -H -- "$@"
}
run_sudo_install() {
	min_args 5 "$@"
	local mode=$1
	local owner=$2
	local group=$3
	shift 3
	run_sudo install --mode $mode --owner $owner --group $group "$@"
}
seed_sudo() { sudo -s </dev/null; }
pipe_to_sudo() { sudo -s; }
sudo_pipe_to_file() {
	has_args 1 "$@"
	tmp=$(cmd_tempfile)
	run cat >$tmp
	run_sudo mv $tmp $1
}

run_editor() {
	[ "$EDITOR" ] || error "\$EDITOR is not set"
	run $EDITOR "$@"
}

run_pager() {
	[ "$PAGER" ] || error "\$PAGER is not set"
	run clear
	run $PAGER "$@"
}