From 512d6172e337bbbe28cc76b8221b7b409742e462 Mon Sep 17 00:00:00 2001
From: Andy C
Date: Wed, 15 Dec 2021 00:34:31 -0500
Subject: [PATCH] [soil] Update home page
Turned up https://builds.oilshell.org/
To receive build results from multiple services. Working toward #1038.
---
soil/web-init.sh | 88 +++++++++++++++++++++++++++++++++++++-----------
1 file changed, 69 insertions(+), 19 deletions(-)
diff --git a/soil/web-init.sh b/soil/web-init.sh
index d76ed72806..aab02bc437 100755
--- a/soil/web-init.sh
+++ b/soil/web-init.sh
@@ -22,7 +22,8 @@ source soil/common.sh # for USER and HOST
home-page() {
### travis-ci.oilshell.org home page
- local title='Soil on travis-ci.oilshell.org'
+ local domain=${1:-'travis-ci.oilshell.org'}
+ local title="Soil on $domain"
soil-html-head "$title"
cat <Soil for details.
-
+