2023-04-24 21:37:58 +03:00
|
|
|
The `switch` command switches to an existing project or branch.
|
|
|
|
|
|
|
|
Setup stuff.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-24 21:37:58 +03:00
|
|
|
someterm = 18
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-24 21:37:58 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-24 21:37:58 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
someterm : Nat
|
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-24 21:37:58 +03:00
|
|
|
foo/main> add
|
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
someterm : Nat
|
|
|
|
|
2023-05-01 20:48:27 +03:00
|
|
|
foo/main> branch bar
|
|
|
|
|
|
|
|
Done. I've created the bar branch based off of main.
|
|
|
|
|
2024-04-24 19:29:15 +03:00
|
|
|
Tip: To merge your work back into the main branch, first
|
2024-05-01 20:18:46 +03:00
|
|
|
`switch /main` then `merge /bar`.
|
2023-05-01 20:48:27 +03:00
|
|
|
|
2023-04-24 21:37:58 +03:00
|
|
|
foo/main> branch topic
|
|
|
|
|
|
|
|
Done. I've created the topic branch based off of main.
|
|
|
|
|
2024-04-24 19:29:15 +03:00
|
|
|
Tip: To merge your work back into the main branch, first
|
2024-05-01 20:18:46 +03:00
|
|
|
`switch /main` then `merge /topic`.
|
2023-04-24 21:37:58 +03:00
|
|
|
|
|
|
|
```
|
2023-05-01 20:48:27 +03:00
|
|
|
Now, the demo. When unambiguous, `switch` switches to either a project or a branch in the current project. A branch in
|
2023-05-02 23:30:24 +03:00
|
|
|
the current project can be preceded by a forward slash (which makes it unambiguous). A project can be followed by a
|
|
|
|
forward slash (which makes it unambiguous).
|
2023-04-24 21:37:58 +03:00
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> switch foo
|
2023-04-24 21:37:58 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> switch foo/topic
|
2023-04-24 21:37:58 +03:00
|
|
|
|
2023-05-01 20:48:27 +03:00
|
|
|
foo/main> switch topic
|
|
|
|
|
|
|
|
foo/main> switch /topic
|
|
|
|
|
2023-05-02 23:30:24 +03:00
|
|
|
foo/main> switch bar/
|
|
|
|
|
2023-05-01 20:48:27 +03:00
|
|
|
```
|
|
|
|
It's an error to try to switch to something ambiguous.
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-05-01 20:48:27 +03:00
|
|
|
foo/main> switch bar
|
|
|
|
|
2023-05-04 01:22:50 +03:00
|
|
|
I'm not sure if you wanted to switch to the branch foo/bar or
|
|
|
|
the project bar. Could you be more specific?
|
2023-05-01 22:16:01 +03:00
|
|
|
|
2023-05-04 01:22:50 +03:00
|
|
|
1. /bar (the branch bar in the current project)
|
|
|
|
2. bar/ (the project bar, with the branch left unspecified)
|
2023-05-01 22:16:01 +03:00
|
|
|
|
|
|
|
Tip: use `switch 1` or `switch 2` to pick one of these.
|
2023-05-01 20:48:27 +03:00
|
|
|
|
2023-04-24 21:37:58 +03:00
|
|
|
```
|
2023-05-01 20:48:27 +03:00
|
|
|
It's an error to try to switch to something that doesn't exist, of course.
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> switch foo/no-such-branch
|
2023-04-24 21:37:58 +03:00
|
|
|
|
|
|
|
foo/no-such-branch does not exist.
|
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> switch no-such-project
|
2023-04-24 21:37:58 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
Neither project no-such-project nor branch /no-such-project
|
|
|
|
exists.
|
2023-04-24 21:37:58 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-05-01 20:48:27 +03:00
|
|
|
foo/main> switch no-such-project-or-branch
|
|
|
|
|
|
|
|
Neither project no-such-project-or-branch nor branch
|
2023-05-02 18:48:16 +03:00
|
|
|
/no-such-project-or-branch exists.
|
2023-05-01 20:48:27 +03:00
|
|
|
|
|
|
|
```
|