diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-15 23:05:44 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-15 21:05:44 +0000 |
| commit | 3564c3345d7fa53744661d815cbd463cc02567d7 (patch) | |
| tree | 6e3a9b3c2b5194ce519083f0d54e128d24521aa2 /.mailmap | |
| parent | 77bca094a140b35341257f125a55212ff0108250 (diff) | |
Avoid options listener for resource manager. (#6366)
This PR simplifies how the resource manager interacts with the options. Instead of using some notification mechanism, the resource manager simply retrieves the options via options::xyz(). This simplifies the options handler, the resource manager interface and the options.
When instructed to do so by the API, the SmtEngine now overwrites the respective option instead of calling out to the resource manager.
Diffstat (limited to '.mailmap')
0 files changed, 0 insertions, 0 deletions