diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 15:20:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-24 18:03:56 +0100 |
| commit | 1161ccf74578c3190d296dc37f39edecf28cf078 (patch) | |
| tree | 852666e60de305821eb94cdeadb1923f45b87fed /printing/genprint.mli | |
| parent | e59d58b6db222332f7d7ad2adcb2b78c24fb351e (diff) | |
Printing again "intros **" as "intros" by default.
The rationale it that it is more common to do so and thus more
"natural" (principle of writing less whenever possible).
Diffstat (limited to 'printing/genprint.mli')
0 files changed, 0 insertions, 0 deletions