From 26f16658cf182139f43822152ef9bd1c817aa69c Mon Sep 17 00:00:00 2001 From: Arnaud Vergnet Date: Tue, 3 Nov 2020 16:47:25 +0100 Subject: [PATCH] use vscodium instead of vscode --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 876857b..177b5e5 100644 --- a/Makefile +++ b/Makefile @@ -7,7 +7,7 @@ format: ocp-indent --inplace src/* edit: - code . -n + codium . -n demo: build @echo "\n==== EXECUTING ====\n"