diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-12 16:09:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-12 16:09:04 +0200 |
| commit | 1671fae4a020a66e329b9ea04c7e06aa13c71d1e (patch) | |
| tree | 49085e71e3831ea16119362a4f87057e95c8f874 /plugins/ssr | |
| parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) | |
Fixing the 3 cases of a "Stream.Error" ended with two periods.
The "Stream.Error" printer does add a period, so, the messages
themselves should not.
Diffstat (limited to 'plugins/ssr')
0 files changed, 0 insertions, 0 deletions