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