Put URL in separate config to avoid Git change

.gitignore

@@ -3,3 +3,4 @@ __pycache__/
 *.pyc
 *.bak
 *~
+/config

README.md

@@ -1,5 +1,4 @@
-To run in development mode, change `MATTERMOST_REMOTE` in `rundev.sh` to a server where you have an
-account, then execute `rundev.sh`.
+To run in development mode, execute `rundev.sh`.
 This will start a web server, and mitmproxy to avoid CORS problems.
 Dependencies for that: Bash, Python and [`mitmproxy`](https://mitmproxy.org/).
 

rundev.sh

@@ -1,18 +1,23 @@
 #!/bin/bash
-
-
-# Config
-MATTERMOST_REMOTE="https://gitlab.mattermost.com"
-
-
-
 set -euo pipefail
 
 cd "$(dirname "$0")"
+
+check_remote() {
 	if [[ $MATTERMOST_REMOTE == */ ]]; then
 		echo "MATTERMOST_REMOTE should not end with a slash (it should only the protocol and the domain; no path)" >&2
 		exit 1
 	fi
+}
+
+if [[ ! -f config ]]; then
+	read -p 'Server URL (e.g. `https://mattermost.example.com`): ' MATTERMOST_REMOTE
+	check_remote
+	echo "MATTERMOST_REMOTE='$MATTERMOST_REMOTE'" > config
+	echo 'You can change this later by editing the file `config`.'
+fi
+source "config"
+check_remote
 
 server_pid=0
 finish() {