Skip to content
This repository has been archived by the owner on Sep 1, 2019. It is now read-only.

Fix #13: deduplicate pull request merge and push information #14

Merged
merged 1 commit into from
Oct 6, 2018
Merged

Fix #13: deduplicate pull request merge and push information #14

merged 1 commit into from
Oct 6, 2018

Commits on Oct 6, 2018

  1. Fix OpenTTD#13: deduplicate pull request merge and push information 

    When a PR is merged, there is no need to show the pushes it caused.
If anyone is interested, they can open up the PR for more
information. As the PR is more interesting than the pushes, the
latter is now ignored if it follows a PR merge.
    @TrueBrain
    TrueBrain committed Oct 6, 2018
    Configuration menu
    Copy the full SHA
    e357be5 View commit details
    Browse the repository at this point in the history