zed/script/start-local-collaboration

40 lines
1,021 B
Text
Raw Normal View History

2022-11-29 22:50:12 +00:00
#!/bin/bash
set -e
if [[ -z "$GITHUB_TOKEN" ]]; then
cat <<-MESSAGE
Missing \`GITHUB_TOKEN\` environment variable. This token is needed
for fetching your GitHub identity from the command-line.
Create an access token here: https://github.com/settings/tokens
Then edit your \`~/.zshrc\` (or other shell initialization script),
adding a line like this:
export GITHUB_TOKEN="(the token)"
MESSAGE
exit 1
fi
github_login=$(curl -sH "Authorization: bearer $GITHUB_TOKEN" https://api.github.com/user | jq -r .login)
other_github_login=nathansobo
if [[ $github_login == $other_github_login ]]; then
other_github_login=as-cii
fi
export ZED_ADMIN_API_TOKEN=secret
export ZED_SERVER_URL=http://localhost:8080
export ZED_WINDOW_SIZE=800,600
cargo build
sleep 0.1
2022-11-29 22:50:12 +00:00
trap "trap - SIGTERM && kill -- -$$" SIGINT SIGTERM EXIT
ZED_WINDOW_POSITION=0,0 ZED_IMPERSONATE=${github_login} target/debug/Zed $@ &
sleep 0.1
ZED_WINDOW_POSITION=800,0 ZED_IMPERSONATE=${other_github_login} target/debug/Zed &
sleep 0.1
2022-11-29 22:50:12 +00:00
wait