Skip to content
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

Update documentation for multiple selection #12

Closed
wants to merge 7 commits into from
Closed

Update documentation for multiple selection #12

wants to merge 7 commits into from

Conversation

firezym
Copy link
Contributor

@firezym firezym commented Dec 3, 2023

Update documentation for multiple selection, including:

  1. gif demonstration
  2. mentioning it in doc

update documentation for multiple selection
trivial lint
@parmentelat
Copy link
Owner

oops I forgot to push my latest commits...
would you care to rebase on top of the latest main ?
my bad...

@firezym
Copy link
Contributor Author

firezym commented Dec 3, 2023

no problem. I will sync again.

@firezym
Copy link
Contributor Author

firezym commented Dec 3, 2023

Is there a need to rebase? Just now I have merged your newest commits. Seems no conflicts. I think maybe we can pass the check now.

@parmentelat
Copy link
Owner

yeah I meant to rebase, not to merge
never mind, I did it on my end, no worries
will issue 0.2.4 shortly

@firezym
Copy link
Contributor Author

firezym commented Dec 3, 2023

Alright. Thanks :)

@firezym
Copy link
Contributor Author

firezym commented Dec 10, 2023

@parmentelat It seems that your README.md page is not updated of the newest gif demo. My PR is 4 commits ahead. What should I do to help sync?

@parmentelat
Copy link
Owner

hey @firezym

3 things:

  • first, the content is fine; it's true that the multi-cell sequence comes very (too ?) late in the gif, but please double-check, it's there; it came as part of my rebase with commit a500d0d
  • second, I had again forgotten to push the very last commit 47fb0be, I just did that; mind you, it was just about the new release numbers...
  • last, as I said I rebased the repo on my end, so you have to give up on your merge !
    otherwise you're going to weave a branch that is endlessly parallel to mine...
    if you're not too fluent with git the simplest is maybe to just trash your fork and create a new one..

@firezym firezym closed this by deleting the head repository Dec 10, 2023
@firezym
Copy link
Contributor Author

firezym commented Dec 10, 2023

@parmentelat I checked all the changes. It is already the newest in your repo. So I just deleted my fork ... too complicated for me to understand the parallel universe ... maybe I should ask Loki about it later... lol,

@parmentelat
Copy link
Owner

sounds about right ! thanks

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