Differences between revisions 9 and 10
Revision 9 as of 2020-06-30 09:39:05
Size: 2992
Comment: fix example
Revision 10 as of 2020-06-30 09:44:04
Size: 2934
Comment: change tags to lightweight tags in example
Deletions are marked like this. Additions are marked like this.
Line 26: Line 26:
 * git tag -a issue999-base -m "add tag issue999-base" <rev>
 * git tag -a issue999-v1 -m "add tag issue999-v1" <rev>
 * git tag issue999-base <rev>
 * git tag issue999-v1 <rev>

Back to developer page.

Git

Our Git workflow (work in progress)

Outcome of the discussion in the Fast Downward meeting on 21 February:

Best practices:

  • TODO: git bisect with --first-parent etc. (Malte sent a few links)
  • TODO: how to configure git + meld
  • TODO: can we use github's facilities on the webpage for, e.g., merging pull requests or does this do "wrong" things?

Suggested workflow:

  • git checkout -b issue999
  • ...
  • git commit -m "[issue999] some changes"
  • ...
  • git tag issue999-base <rev>

  • git tag issue999-v1 <rev>

  • git push --set-upstream origin issue999 --tags
  • ...
  • git checkout main
  • git merge --no-ff issue999
  • git branch -d issue999
  • git push

.gitconfig file:

[merge]
tool = meld

[mergetool "meld"]
#cmd = meld "$LOCAL" "$BASE" "$REMOTE" --output "$MERGED"
cmd = meld "$LOCAL" "$MERGED" "$REMOTE" --output "$MERGED"

[diff]
tool = meld

[difftool "meld"]
cmd = meld "$LOCAL" "$REMOTE"

[difftool]
prompt = false

[alias]
ci = commit
st = status
meld = difftool

# aliases that match the hg in / out commands
out = !git fetch && git log FETCH_HEAD..
in = !git fetch && git log ..FETCH_HEAD
  • [Silvan] I also found out that meld actually knows about hg/git, so instead of configuring above and typing hg meld/git meld, one could also just type meld .
  • [Silvan] Unfortunately, I haven't found a way for git merge to automatically open meld instead of first doing an incomplete merge and then viewing the failed merge via hg mergetool, which, if configured as above to take $MERGED as the middle file, contains the failed merge in the >>>> ... <<<< ... format, which I really don't like. If anyone finds out how to let git automatically merge what it can and then immediately prompt the user via mergetool instead of requiring this to be called manually, and even better, without showing the failed merge, I would be very happy.

FastDownward: ForDevelopers/Git (last edited 2023-02-14 15:29:06 by SilvanSievers)