diff options
Diffstat (limited to 'toplevel/ide_blob.mli')
| -rw-r--r-- | toplevel/ide_blob.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli index b1261e496..34879f057 100644 --- a/toplevel/ide_blob.mli +++ b/toplevel/ide_blob.mli @@ -43,6 +43,4 @@ val current_goals : goals call val read_stdout : string call -val contents : Lib.library_segment call - val loop : unit -> unit |