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") )
|
2021-12-16 22:04:50 +00:00
|
|
|
echo "Editing $@..."
|
2020-11-22 18:55:59 +00:00
|
|
|
if test -w "$1" || (test ! -f "$1" && test -w $(dirname "$1"))
|
2021-12-16 22:04:50 +00:00
|
|
|
then $EDITOR "$@"
|
|
|
|
else sudoedit "$@"
|
2020-11-22 18:55:59 +00:00
|
|
|
fi
|