File indexing completed on 2024-05-05 17:36:17
0001 #!/bin/sh 0002 0003 HAS_SIZE='' 0004 HAS_AUTO='' 0005 0006 while read -r line 0007 do 0008 # substring from beginning to equal sign 0009 ENTRY="${line%%=*}" 0010 if [ "$ENTRY" = "BorderSize" ]; then 0011 HAS_SIZE=1 0012 fi 0013 if [ "$ENTRY" = "BorderSizeAuto" ]; then 0014 HAS_AUTO=1 0015 fi 0016 echo "$line" 0017 done 0018 0019 if [ -n "$HAS_SIZE" -a -z "$HAS_AUTO" ]; then 0020 # unset auto borders if user has set a border 0021 # size in the past (for good measure make 0022 # also sure auto borders are not yet set) 0023 echo "BorderSizeAuto=false" 0024 fi