From b16dedd9de42fd83e13332c0ea93fd2f5a60ee09 Mon Sep 17 00:00:00 2001
From: Alessandro Pignotti <a.pignotti@sssup.it>
Date: Mon, 22 May 2023 17:18:28 +0200
Subject: [PATCH] Restore reasonable defaults for local deployment

---
 index.html | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/index.html b/index.html
index c8da6b5..e29ea89 100644
--- a/index.html
+++ b/index.html
@@ -245,11 +245,20 @@ __      __   _  __   ____  __
 	function runBash()
 	{
 		// cmd, cwd, args and env are replaced by the Github actions workflow.
+		var cmd = CMD;
+		var args = ARGS;
+		var env = ENV;
+		var cwd = CWD;
+		// Reasonable defaults for local deployments
+		// cmd = "/bin/bash";
+		// args = ["--login"];
+		// env = ["HOME=/home/user", "TERM=xterm", "USER=user", "SHELL=/bin/bash", "EDITOR=vim", "LANG=en_US.UTF-8", "LC_ALL=C"];
+		// cwd = "/home/user";
 		const structure = {
-			cmd: CMD,
-			args: ARGS,
-			env: ENV,
-			cwd: CWD
+			cmd: cmd,
+			args: args,
+			env: env,
+			cwd: cwd
 		}
 		if (typeof SharedArrayBuffer === "undefined")
 		{