Issue1223

[FlorianPommerening]

Adds documentation for the translator options

[roeger]

I had a look at the pull request and only have two small comments.

But wouldn't it make sense to split this into two separate pull requests, one for the renaming in the translator and one for the translator option documentation?

[roeger]

This leads to a very ugly table of contents on the right-hand side, where the options are listed with their parameters (and truncated).

Can we augment the subheadings with a short version for the toc? For example:

### `--invariant-generation-max-time INVARIANT_GENERATION_MAX_TIME` {: data-toc-label="--invariant-generation-max-time"}

[grucla]

I like the idea of having shorter names in the table of contents but I do not know how we could implement this (probably because I do not know how the website generates the table of contents).

[roeger]

That's why I gave the example. I just added the corresponding commit. @FlorianPommerening or @grucla If you think this change is ok, you can from my side merge the pull request.

[grucla]

I'm fine with merging as well.

[FlorianPommerening]

But wouldn't it make sense to split this into two separate pull requests, one for the renaming in the translator and one for the translator option documentation?

We said on Discord that we would treat the renaming as drive-by clean-up unless it needs more discussion. Do you think it does?

[roeger]

But wouldn't it make sense to split this into two separate pull requests, one for the renaming in the translator and one for the translator option documentation?

We said on Discord that we would treat the renaming as drive-by clean-up unless it needs more discussion. Do you think it does?

I don't think it is controversial but it feels like half of the change set.

[FlorianPommerening]

But wouldn't it make sense to split this into two separate pull requests, one for the renaming in the translator and one for the translator option documentation?

We said on Discord that we would treat the renaming as drive-by clean-up unless it needs more discussion. Do you think it does?

I don't think it is controversial but it feels like half of the change set.

Fine with me, but in this case I suggest we go ahead with this issue before doing the renaming. We'll have to cherry-pick the commits that do the renaming from this branch to a new branch and revert them here. I would treat the renaming as not in scope of the sprint story if we don't do it as "drive-by".

[roeger]

Fine with me.

[roeger]

I reverted the changes to the translator here and moved them into a separate PR #300.