Skip to content

Commit 2e6882a

Browse files
committedMay 5, 2025·
Auto merge of #140664 - RalfJung:miri-sync, r=RalfJung
Miri subtree update r? `@ghost`
2 parents 0f73f0f + 4b8f88b commit 2e6882a

File tree

143 files changed

+1796
-1541
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

143 files changed

+1796
-1541
lines changed
 

‎src/tools/miri/.gitignore

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@ tex/*/out
99
*.mm_profdata
1010
perf.data
1111
perf.data.old
12-
flamegraph.svg
12+
flamegraph*.svg
13+
rustc-ice*.txt
1314
tests/native-lib/libtestlib.so
1415
.auto-*
16+
17+
/genmc/

‎src/tools/miri/CONTRIBUTING.md

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,10 @@ When you get a review, please take care of the requested changes in new commits.
1919
existing commits. Generally avoid force-pushing. The only time you should force push is when there
2020
is a conflict with the master branch (in that case you should rebase across master, not merge), and
2121
all the way at the end of the review process when the reviewer tells you that the PR is done and you
22-
should squash the commits. For the latter case, use `git rebase --keep-base ...` to squash without
23-
changing the base commit your PR branches off of. Use your own judgment and the reviewer's guidance
24-
to decide whether the PR should be squashed into a single commit or multiple logically separate
25-
commits. (All this is to work around the fact that Github is quite bad at dealing with force pushes
26-
and does not support `git range-diff`. Maybe one day Github will be good at git and then life can
27-
become easier.)
22+
should squash the commits. If you are unsure how to use `git rebase` to squash commits, use `./miri
23+
squash` which automates the process but leaves little room for customization. (All this is to work
24+
around the fact that Github is quite bad at dealing with force pushes and does not support `git
25+
range-diff`. Maybe one day Github will be good at git and then life can become easier.)
2826

2927
Most PRs bounce back and forth between the reviewer and the author several times, so it is good to
3028
keep track of who is expected to take the next step. We are using the `S-waiting-for-review` and

0 commit comments

Comments
 (0)
Please sign in to comment.