From 053f86fd83331c0ba5a106dc77d754777ccd80dc Mon Sep 17 00:00:00 2001 From: Malte Brandy Date: Thu, 17 Feb 2022 19:33:55 +0100 Subject: [PATCH] Remove unnecessary option --- home-manager/roles/tinkering.nix | 1 - 1 file changed, 1 deletion(-) diff --git a/home-manager/roles/tinkering.nix b/home-manager/roles/tinkering.nix index 81b49cb5..43267d36 100644 --- a/home-manager/roles/tinkering.nix +++ b/home-manager/roles/tinkering.nix @@ -40,7 +40,6 @@ "editor.tabSize" = 3; "editor.fontLigatures" = true; "workbench.colorTheme" = "Default Light+"; - "gitlens.hovers.currentLine.over" = "line"; "workbench.iconTheme" = "material-icon-theme"; "update.mode" = "none"; "update.showReleaseNotes" = false;