summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-06-07 13:56:06 -0700
committerGitHub <noreply@github.com>2018-06-07 13:56:06 -0700
commite0bdf8d71dca4af530273ede2bdd252ca6d8e6b1 (patch)
tree395661187380bd9f8f2866ba31f7b19c93efce3d /src
parent98b41576dcaaa3a6f935613fb7cc9065f4b3b813 (diff)
Look for cryptominisat5_simple, not cryptominisat5 (#2058)
If the boost program_options library is missing, CryptoMiniSat5 only builds a cryptominisat5_simple binary and omits the cryptominisat5, which has more command-line options. We do not use the binary anyway, so this commit changes the cryptominisat.m4 script to look for the cryptominisat5_simple binary, which is always generated.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback