2020-11-22 18:55:59 +00:00
|
|
|
#!/bin/sh
|
2021-07-29 14:02:20 +00:00
|
|
|
# Edit a file with appropriate rights, creating parent directories if necessary
|
2020-11-22 18:55:59 +00:00
|
|
|
test ! -f "$1" && ( mkdir -p $(dirname "$1") || sudo mkdir -p $(dirname "$1") )
|
|
|
|
|
echo "Editing $1..."
|
|
|
|
|
if test -w "$1" || (test ! -f "$1" && test -w $(dirname "$1"))
|
|
|
|
|
then $EDITOR "$1"
|
|
|
|
|
else sudoedit "$1"
|
|
|
|
|
fi
|
