mirror of
https://github.com/martinvonz/jj.git
synced 2024-09-11 13:56:29 +03:00
f72e53376f
According to asciinema.org, it should be possible to change the title after uploading, but I couldn't figure out how to do that. Let's set it when creating the recording. That also means it's one less step to perform when re-running scripts.
22 lines
506 B
Bash
Executable File
22 lines
506 B
Bash
Executable File
#!/bin/bash
|
|
set -euo pipefail
|
|
. "$(dirname "$0")"/demo_helpers.sh
|
|
parse_args "$@"
|
|
|
|
new_tmp_dir
|
|
|
|
run_demo 'Clone a Git repo' '
|
|
run_command "# Clone a Git repo:"
|
|
run_command "jj git clone https://github.com/octocat/Hello-World"
|
|
run_command "cd Hello-World"
|
|
sleep 1
|
|
run_command "# Inspect it:"
|
|
sleep 1
|
|
run_command "jj log"
|
|
sleep 5
|
|
run_command "jj diff -r b1"
|
|
sleep 2
|
|
run_command "# The repo is backed by the actual Git repo:"
|
|
run_command "git --git-dir=.jj/store/git log --graph --all --decorate --oneline"
|
|
'
|