mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
Port empty-namespaces to projects
This commit is contained in:
parent
2fd585e1d3
commit
6a1ccd5a64
@ -31,9 +31,9 @@ scratch/main> history mynamespace
|
||||
Merging an empty namespace should be a no-op
|
||||
|
||||
```ucm:error
|
||||
scratch/main empty> history
|
||||
scratch/main empty> merge.old .mynamespace
|
||||
scratch/main empty> history
|
||||
scratch/main> history empty
|
||||
scratch/main> merge.old empty .mynamespace
|
||||
scratch/main> history empty
|
||||
```
|
||||
|
||||
Add and then delete a term to add some history to a deleted namespace.
|
||||
|
@ -58,21 +58,19 @@ scratch/main> history mynamespace
|
||||
Merging an empty namespace should be a no-op
|
||||
|
||||
```ucm
|
||||
☝️ The namespace .empty is empty.
|
||||
scratch/main> history empty
|
||||
|
||||
.empty> history
|
||||
☝️ The namespace empty is empty.
|
||||
|
||||
☝️ The namespace .empty is empty.
|
||||
|
||||
.empty> merge.old .mynamespace
|
||||
scratch/main> merge.old empty .mynamespace
|
||||
|
||||
⚠️
|
||||
|
||||
The namespace .mynamespace doesn't exist.
|
||||
The namespace empty doesn't exist.
|
||||
|
||||
.empty> history
|
||||
scratch/main> history empty
|
||||
|
||||
☝️ The namespace .empty is empty.
|
||||
☝️ The namespace empty is empty.
|
||||
|
||||
```
|
||||
Add and then delete a term to add some history to a deleted namespace.
|
||||
|
Loading…
Reference in New Issue
Block a user