[m-rev.] [PATCH 4/4] Delete unused type io.stream_putback.
Peter Wang
novalazy at gmail.com
Tue Jul 22 15:00:26 AEST 2014
library/io.m:
As above.
---
library/io.m | 2 --
1 file changed, 2 deletions(-)
diff --git a/library/io.m b/library/io.m
index d9646f9..54f9e6c 100644
--- a/library/io.m
+++ b/library/io.m
@@ -1777,8 +1777,6 @@
public static univ.Univ_0 ML_io_user_globals = null;
").
-:- type io.stream_putback == map(io.stream_id, list(char)).
-
:- type io.input_stream ---> input_stream(io.stream).
:- type io.output_stream ---> output_stream(io.stream).
--
1.8.4
More information about the reviews
mailing list