Fix #991: Add a gap between workspaces when swiping/navigating (#996)

This commit is contained in:
José Expósito 2020-12-21 18:44:17 +01:00 committed by GitHub
parent bb573b409a
commit fd98933ed1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -102,6 +102,8 @@ namespace Gala {
private bool animating_switch_workspace = false;
private GestureAnimationDirector gesture_animation_director;
private const int WORKSPACE_GAP = 24;
construct {
gesture_animation_director = new GestureAnimationDirector ();
@ -2107,6 +2109,7 @@ namespace Gala {
main_container.height = move_primary_only ? monitor_geom.height : screen_height;
var x2 = move_primary_only ? monitor_geom.width : screen_width;
x2 += WORKSPACE_GAP * InternalUtils.get_ui_scaling_factor ();
if (direction == Meta.MotionDirection.RIGHT)
x2 = -x2;