Merge request 10 (8374751a1fdf1759df5a4c61806d0501c50866e3 -> c25d7a40770df4e6adc9271189db9bc26dddc2d0)
By: anonymous
Against ref: refs/heads/master
Date: 2020-03-01 17:53
Already merged at 2020-03-01 17:53 UTC.
Commit c25d7a40770df4e6adc9271189db9bc26dddc2d0
- update end
Author: fugohan
Author date (UTC): 2020-03-01 17:53
Committer name: fugohan
Committer date (UTC): 2020-03-01 17:53
Parent(s): 8374751a1fdf1759df5a4c61806d0501c50866e3
Signer:
Signing key:
Signing status: N
Tree: dcd7eae7cb28802d7b1d4d428406db7e6af72a97
File latexout.tex changed (mode: 100644) (index c4fc01d..a7b4b3f) |
6 |
6 |
\begin{document} |
\begin{document} |
7 |
7 |
\section{Binomische Form} |
\section{Binomische Form} |
8 |
8 |
\input{latexout2.tex} |
\input{latexout2.tex} |
9 |
|
\end{document} |
|
10 |
|
|
|
11 |
|
%test 2 |
|
|
9 |
|
\end{document}%end |
Hints:
How to merge on your machine?
git fetch origin refs/mr/10:mr-10
git checkout main
git merge mr-10
To "see" all the merge requests as branches,
add, in the config file (.git/config), under the remote you want,
a line like this:
fetch = +refs/mr/*:refs/remotes/your_remote_name_for_example_origin/mr/*
After you run a git fetch, you will have all the pull requests locally.
For example, you can merge one of them:
git checkout main
git merge mr/10