Ensure word usage is consistent

• Option: a command line option
• Strategy: a specific set of command line options
• Schedule: A list of strategies, timeout pairs

unassigned @hschurr

By Hans-Jörg Schurr on 2021-03-02T15:57:53 (imported from GitLab)

created merge request !2 (closed) to address this issue

By Hans-Jörg Schurr on 2021-12-26T15:56:40 (imported from GitLab)

mentioned in merge request !2 (closed)

By Hans-Jörg Schurr on 2021-12-26T15:56:41 (imported from GitLab)

Done I think.

By Hans-Jörg Schurr on 2021-12-26T15:57:06 (imported from GitLab)