diff options
Diffstat (limited to 'ide/utils/config_file.ml')
| -rw-r--r-- | ide/utils/config_file.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 4d0aabeb6..e4c613913 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -44,9 +44,6 @@ (* ******************************************************************************** *) (* This code is intended to be usable without any dependencies. *) -(* pipeline style, see for instance Raw.of_channel. *) -let (|>) x f = f x - (* as List.assoc, but applies f to the element matching [key] and returns the list where this element has been replaced by the result of f. *) let rec list_assoc_remove key f = function |