Workshop

[zpopov]

Changes made to the weblinks.
Thanks

[zpopov]

I am probably pain right now but I am learning :-)

[robertoostenveld]

bummer. I was just too late with my last comment on #757. I'll fix the conflict.

[robertoostenveld]

I have merged the conflicting versions, please do a git pull before you make any other change

[zpopov]

Do I need to Close the pull request now, which then signals to you guys the merge request? Or is it good now?

[robertoostenveld]

no you should not close it! It will close automatically when I merge.

If you were to close prior to merge, I would assume that the proposed change does not apply any more and that it is to be discarded.

If you want to use the github pull request to flag to me (remotely) when to merge (as you working on it takes some time), then you should first submit the pull request in draft mode. In that mode, the PR cannot be merged by me yet. If you then switch from draft to open, that would flag to me that it is ready for review, I review, I merge and then it automatically closes.

[robertoostenveld]

Let me merge this one, as I think it is ready.