Closed ruphy closed 2 years ago
Hi, @ruphy. Would it be useful to you for us to merge this PR? I'm happy to do so, if it'll make integration with Overleaf easier for you.
Hello @kfogel! indeed, the integration is not possible as long as the PR is not merged as the history are technically separated. A merge commit would allow it to operate on a compatible tree
@ruphy +1 on the merge. By the way, I just renamed our default branch from master
to main
(I did this after your merge, so there should be no problem).
Hi, I managed to merge the histories of the Overleaf document we will be using for reviews and the history of this GitHub repository. This Pull Request adds a dummy file and reverts it: leaving the repository content unchanged, now, with a unique history, we are able to push new commits directly into the Overleaf document.