diff options
Diffstat (limited to 'src/print.sig')
| -rw-r--r-- | src/print.sig | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/print.sig b/src/print.sig index 39daf5d0..07b8c1e2 100644 --- a/src/print.sig +++ b/src/print.sig @@ -30,6 +30,8 @@ signature PRINT = sig structure PD : PP_DESC where type PPS.token = string + and type PPS.device = TextIOPP.device + and type PPS.stream = TextIOPP.stream type 'a printer = 'a -> PD.pp_desc |