add link to reddit (and a tweak)

[web.git] / ralf / _posts / 2022-07-02-miri.md

diff --git a/ralf/_posts/2022-07-02-miri.md b/ralf/_posts/2022-07-02-miri.md
index 1108e0d452a88de0a11fa6d60074fb4e78a4f7fa..78f4bbb4bc34ae6dd87d8a48f8a2d20befd79925 100644 (file)
--- a/ralf/_posts/2022-07-02-miri.md
+++ b/ralf/_posts/2022-07-02-miri.md
@@ -1,6 +1,7 @@
 ---
 title: "The last two years in Miri"
 categories: rust
+reddit: /rust/comments/vq3mmu/the_last_two_years_in_miri/
 ---
 
 It has been [almost two years]({% post_url 2020-09-28-miri %}) since my last Miri status update.
@@ -179,8 +180,9 @@ Miri is not *truly* random, but uses a pseudo-random number generator to make al
 This means you can explore various different possible choices by passing different *seeds* for Miri to use for its pseudo-random number generator.
 The following little shell snippet will run Miri with many different seeds, which is great to be able to locally reproduce a failure that you saw on CI, but that you are having trouble reproducing:
 ```
-for seed in $({ echo obase=16; seq 0 255; } | bc); do
-  MIRIFLAGS="-Zmiri-seed=$seed" cargo miri test || { echo "Failing seed: $seed"; break; };
+for SEED in $({ echo obase=16; seq 0 255; } | bc); do
+  echo "Trying seed: $SEED"
+  MIRIFLAGS=-Zmiri-seed=$SEED cargo miri test || { echo "Failing seed: $SEED"; break; };
 done
 ```
 It is important that you use exactly the same `MIRIFLAGS` as CI to ensure the failure can even happen!