diff options
| author | Mike Krüger <mkrueger@xamarin.com> | 2013-03-02 15:58:14 +0400 |
|---|---|---|
| committer | Mike Krüger <mkrueger@xamarin.com> | 2013-03-02 15:58:14 +0400 |
| commit | a57069cd301bf06a7555a353abbc052ca742df9a (patch) | |
| tree | bff04c3c03256a6f26f8c5f5fc7aea6aa2ffe68e /main/monodevelop.in | |
| parent | 9c83c6e84cb3d8f49e9c0cf92ed22876cce3a923 (diff) | |
[Shell] Disable Ubuntu overlay scrollbars.
They're not very helpful in our user interface.
Diffstat (limited to 'main/monodevelop.in')
| -rwxr-xr-x | main/monodevelop.in | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/main/monodevelop.in b/main/monodevelop.in index cc164681fb..dac25b8633 100755 --- a/main/monodevelop.in +++ b/main/monodevelop.in @@ -3,6 +3,10 @@ #Workaround for Unity gnome shell export UBUNTU_MENUPROXY=0 +# Ubuntu overlay scrollbars are not working well with the 1px boundaries in the monodevelop shell +export LIBOVERLAY_SCROLLBAR=0 + + #this script should be in $PREFIX/bin MONO_EXEC="exec -a monodevelop mono" EXE_PATH="${0%%/bin/monodevelop}/lib/monodevelop/bin/MonoDevelop.exe" |