diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index ffa07ead7..51ae76ff5 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -9,8 +9,6 @@ open Preferences -exception Forbidden - let warn_image () = let img = GMisc.image () in img#set_stock `DIALOG_WARNING; |