From 06bbdfcd174f45b9ae891ab7134476b1e69f467e Mon Sep 17 00:00:00 2001 From: Silvan Sievers Date: Fri, 6 Aug 2021 17:33:18 +0200 Subject: [PATCH] [main] remove duplicate option 'random_seed' --- src/search/merge_and_shrink/merge_tree_factory_linear.cc | 1 - 1 file changed, 1 deletion(-) diff --git a/src/search/merge_and_shrink/merge_tree_factory_linear.cc b/src/search/merge_and_shrink/merge_tree_factory_linear.cc index 9f4b1ee77c..5dcc33ad58 100644 --- a/src/search/merge_and_shrink/merge_tree_factory_linear.cc +++ b/src/search/merge_and_shrink/merge_tree_factory_linear.cc @@ -123,7 +123,6 @@ void MergeTreeFactoryLinear::add_options_to_parser( "variable_order", merge_strategies, "the order in which atomic transition systems are merged", "CG_GOAL_LEVEL"); - utils::add_rng_options(parser); } static shared_ptr _parse(options::OptionParser &parser) {