robertoostenveld
commented
6 years ago since there is a git conflict, I suggest that @hurngchunlee does the merge if @EricMaris agrees.
Closed robertoostenveld closed 6 years ago
robertoostenveld
commented
6 years ago since there is a git conflict, I suggest that @hurngchunlee does the merge if @EricMaris agrees.
I think we should merge master into gh-pages and thereby ensure that obsolete documentation gets deleted.