8000 Use namespace diff in link output by mitchellwrosen · Pull Request #1164 · unisonweb/unison · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Use namespace diff in link output #1164

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 21, 2020

Conversation

mitchellwrosen
Copy link
Member

Here's a screenshot of linking, then undoing (previously link would just say Done.):

Screen Shot 2020-01-20 at 2 29 27 PM

I'm a bit confused by the output... note that contains is called lib.contains when the link is undone. 🤷‍♂

@mitchellwrosen mitchellwrosen force-pushed the mitchell/2020-01-20/improve-link-output branch from 68cce0d to 38fdcd0 Compare January 20, 2020 19:36
@aryairani
Copy link
Contributor
aryairani commented Jan 21, 2020

Cool, yeah sorry for the confusion. The unfortunate reason that is happening is because the diff function takes two namespaces to compare. For link it’s using the old and new namespace at path parent, as you’ve defined it; for undo it’s using the old and new root, so lib shows up in the output.

Since undo generally can be undoing something anywhere or all over, I’m not sure what else we could do here, short of resolving absolute names to maybe-relative ones later than the current pre-baked Name model supports.

@mitchellwrosen
Copy link
Member Author

Gotcha. The link diff could diff the roots, too - but I agree a better fix is to use absolute names everywhere until final rendering

@mitchellwrosen mitchellwrosen merged commit 1fce1d4 into master Jan 21, 2020
@mitchellwrosen mitchellwrosen deleted the mitchell/2020-01-20/improve-link-output branch January 21, 2020 16:09
@aryairani aryairani mentioned this pull request Mar 12, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants
0