diff options
Diffstat (limited to '.wmii/util.sh')
| -rw-r--r-- | .wmii/util.sh | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/.wmii/util.sh b/.wmii/util.sh index 3234783..43d7d4a 100644 --- a/.wmii/util.sh +++ b/.wmii/util.sh @@ -31,6 +31,13 @@ expand_variables() { done } +is_mounted() { + dir="$(readlink -m $1)" + mntpnt="$(cut -d' ' -f2 /proc/mounts|grep -- "$dir")" + [[ $dir = "$mntpnt" ]] + return $? +} + ################################################################################ # PATH manipulation # ################################################################################ |