Reviewed by @burblebee: good

@zygoloid When sources are provided (and have been reviewed by a member), is it OK to create a PR directly like this? Note that the commit message needs to be fixed to P1085R2 Should Span be Regular?

@burblebee For future reference, I'd like the pull request to be moved to a properly-named branch in our repository in a case like this, so that I can amend and rebase it as needed when merging. I'll do that for this one (but it looks like that requires closing this and opening a new PR).

Superseded by #2508.

@burblebee For future reference, I'd like the pull request to be moved to a properly-named branch in our repository in a case like this ...

@zygoloid Thanks for letting me know. How were you able to checkout Tony's commit so that you could create a new branch from it? I can't see his commit from my tree. I get:

$git show 482d0d2c7d66aedcd64337b546b62ec249ca7ded
fatal: bad object 482d0d2c7d66aedcd64337b546b62ec249ca7ded

Is that commit is on tvaneerd's fork? If so, I tried the following based on this from stackoverflow:

git remote add tvaneerd https://github.com/tvaneerd/cplusplus/draft.git
git fetch tvaneerd
git checkout -b mypatch-1 tvaneerd/patch-1

But the fetch results in the error:

remote: Not Found
fatal: repository 'https://github.com/tvaneerd/cplusplus/draft.git/' not found

@jwakely @tvaneerd Any idea what I'm doing wrong?

git remote add tvaneerd https://github.com/tvaneerd/cplusplus/draft.git

The proper remote URL is https://github.com/tvaneerd/draft.git.

There's no need for the remote repository: pull requests are part of the destination repository, and they can be checked out just like any other branch. If you want, you can make a pull request and immediately delete your repository and your github account, and we still have the PR.

@CaseyCarter That URL worked!! Thank you!! :) . So the correct commands are:

git remote add tvaneerd https://github.com/tvaneerd/draft.git
git fetch tvaneerd
git checkout -b mypatch-1 tvaneerd/patch-1

@tvaneerd Apparently creating the PR works also, but I wanted to be able to grab the sources locally before taking that step. Now I know how to do that thanks to Casey :).
That said, I didn't know how to create a local branch from the PR either, but I got a reply from @zygoloid with detailed steps on how he was able to do that:

# grab tony's pull request and put it into a new local branch motions-2018-11-lwg-23
git fetch origin pull/2478/head:motions-2018-11-lwg-23
# switch that branch
git checkout motions-2018-11-lwg-23
# rebase on the current working draft
git rebase master
# and push the branch back with the correct name, setting the remote branch as the 'upstream' of my local branch
git push -u origin motions-2018-11-lwg-23