diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-08 12:28:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-08 12:28:39 +0100 |
| commit | 35219fd89ce9a1b7ce92316ee84e3c8ad40b3831 (patch) | |
| tree | ec678fd5ae4bd8caea13170d57b177f22fd399f9 /lib | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
Fixing an (apparently misplaced) spc in anomaly reporting message.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3f4e8aa12..6d3fdf927 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -91,7 +91,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++ + hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else hov 0 (raw_anomaly e) |