diff options
| author | Enrico Tassi | 2014-07-29 14:34:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-29 14:34:59 +0200 |
| commit | b5c4f505c53113b789db0de82ce2bc1374415d58 (patch) | |
| tree | ca43067643d6f81cbac3f14389ddeb163c0f41ea /lib | |
| parent | 8adafaf8c2f77c44b3202de8aea2bbb36acb0362 (diff) | |
Pp: only one default feedback id
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -428,7 +428,6 @@ let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg (** Feedback *) let feeder = ref ignore -let feedback_id = ref (Feedback.Edit 0) let set_id_for_feedback i = feedback_id := i let feedback ?state_id what = !feeder { |
