diff options
author | Adam Chlipala <adam@chlipala.net> | 2012-05-05 12:45:35 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2012-05-05 12:45:35 -0400 |
commit | 9835be3a1ebfdad7b265a966df45a87555624c95 (patch) | |
tree | 85b4d5ef5bf9c2f5087c15d4d480ea04394dea8a /src/elaborate.sig | |
parent | 20687af11a2d3d1b181b28843a9d45eeadfa680a (diff) |
Send daemon output to calling process
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r-- | src/elaborate.sig | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig index 18e6c3b4..b4a4da88 100644 --- a/src/elaborate.sig +++ b/src/elaborate.sig @@ -42,5 +42,6 @@ signature ELABORATE = sig * early phase. *) val incremental : bool ref + val verbose : bool ref end |