# HG changeset patch
# User desharna
# Date 1648804863 -7200
# Node ID be177eabb64b4fc60df4d5af669c7bbc46e9a53a
# Parent  c2532adbfa3eb87a5a7c992989118c5e3d0e8ced
tuned sledgehammer documentation

diff -r c2532adbfa3e -r be177eabb64b src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Apr 01 09:58:05 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Apr 01 11:21:03 2022 +0200
@@ -1167,6 +1167,10 @@
 Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is
 useful for regression testing.
 
+The expected outcomes are not mutually exclusive. More specifically, \textit{some} is accepted
+whenever \textit{some\_preplayed} is accepted as the former has strictly fewer requirements
+than the later.
+
 \nopagebreak
 {\small See also \textit{timeout} (\S\ref{timeouts}).}
 \end{enum}