diff options
| author | Jakub Beránek <berykubik@gmail.com> | 2025-07-23 09:24:52 +0200 |
|---|---|---|
| committer | Jakub Beránek <berykubik@gmail.com> | 2025-07-23 09:24:52 +0200 |
| commit | a6c10939acdadf274e67f97f1e605b4e563a8c7a (patch) | |
| tree | 722a0473461f1dfbaa621a01ab1fa72fccb8c720 | |
| parent | 7a8288bce479b12f489a2b66b5cee1dfc6ff2e07 (diff) | |
Init josh-sync config file
| -rw-r--r-- | src/tools/miri/josh-sync.toml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/tools/miri/josh-sync.toml b/src/tools/miri/josh-sync.toml new file mode 100644 index 00000000000..86208b3742d --- /dev/null +++ b/src/tools/miri/josh-sync.toml @@ -0,0 +1,2 @@ +repo = "miri" +filter = ":rev(75dd959a3a40eb5b4574f8d2e23aa6efbeb33573:prefix=src/tools/miri):/src/tools/miri" |