From efd9cf2d9b70ad606754876883598a80a627a277 Mon Sep 17 00:00:00 2001 From: Mylloon Date: Thu, 4 Aug 2022 19:18:43 +0200 Subject: [PATCH] use micro as the default editor --- arch.sh | 1 + wsl.sh | 1 + 2 files changed, 2 insertions(+) diff --git a/arch.sh b/arch.sh index 5b01708..de39cbe 100644 --- a/arch.sh +++ b/arch.sh @@ -122,6 +122,7 @@ then # === Micro configuration == git config --global core.editor "micro" + set -Ux EDITOR micro wget -q --show-progress https://git.kennel.ml/Anri/confOS/raw/branch/main/.config/micro/settings.json -O "$HOME"/.config/micro/settings.json micro -plugin install detectindent diff --git a/wsl.sh b/wsl.sh index 548da3e..a13ffa2 100644 --- a/wsl.sh +++ b/wsl.sh @@ -96,6 +96,7 @@ then curl https://getmic.ro | GETMICRO_PLATFORM=linux64 bash cd - || exit git config --global core.editor "micro" + set -Ux EDITOR micro wget -q --show-progress https://git.kennel.ml/Anri/confOS/raw/branch/main/.config/micro/settings.json -O "$HOME"/.config/micro/settings.json micro -plugin install detectindent