Options

Many definitions can have options. These are hints or processing instructions to the various translator tools.

• need more detail