weird-domains branch Bradley Lucier (22 Apr 2022 17:44 UTC)
Re: weird-domains branch Arthur A. Gleckler (22 Apr 2022 23:39 UTC)

weird-domains branch Bradley Lucier 22 Apr 2022 17:44 UTC

Arthur:

I'm not really sure of the development model underlying git, but I'd
like to do something different than in the past.  Maybe you can help.

I'm willing to explore how to refine the procedures we have for empty
and zero-dimensional intervals, but I don't want to make changes
incrementally to the main repository.

Is the way to do it for you to add a weird-domains branch to your
repository, which when I pull from your repository, I will get.  I could
branch from weird-domains in my repository and send you pull requests
for weird-domains when I'm ready to push changes upstream, so we'd be
doing development on weird-domains.

Then, if/when things are finished on weird-domains, you could merge
weird-domains into the main branch.

Do things work this way?  Does that sound reasonable?

Brad