[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