Ubuntu Pastebin

Paste from Paul at Sun, 12 Jul 2015 11:40:09 +0000

Download as text 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
	

    #!/usr/bin/env bash
     
    dir=`dirname $0`
    source $dir/src/tools.sh
     
    get_default_profile() {
      if [ "$newGnome" = "1" ]
        then profile_id="$(dconf read $dconfdir/default | \
            sed s/^\'// | sed s/\'$//)"
        profile_name="$(dconf read $dconfdir/":"$profile_id/visible-name | \
            sed s/^\'// | sed s/\'$//)"
      else
        profile_name="$(gconftool-2 -g \
            /apps/gnome-terminal/global/default_profile)"
      fi
      echo $profile_name
    }
     
    PROFILE=${2:-"$(get_default_profile)"}
    $dir/install.sh -s $1 -p "$PROFILE"
Download as text