diff options
author | Paul E. McKenney <paulmck@kernel.org> | 2019-03-20 14:37:46 -0700 |
---|---|---|
committer | Paul E. McKenney <paulmck@kernel.org> | 2023-03-24 10:24:14 -0700 |
commit | 0838ba7e5b80e593af27bc5b682ee24e9e1e2ca6 (patch) | |
tree | 0b873f073412dcf8d0d46c0b91256b5f61b0a07c /tools/memory-model/scripts/checkghlitmus.sh | |
parent | 579ecb2e4108af3689b1b814fff23f6a69907dab (diff) |
tools/memory-model: Make judgelitmus.sh ransack .litmus.out files
The judgelitmus.sh script currently relies solely on the "Result:"
comment in the .litmus file. This is problematic when using the --hw
argument, because it is necessary to check the hardware model against
LKMM even in the absence of "Result:" comments.
This commit therefore modifies judgelitmus.sh to check the observation
in a .litmus.out file, in case one was generated by a previous LKMM run.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model/scripts/checkghlitmus.sh')
0 files changed, 0 insertions, 0 deletions