aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/source.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 18:17:21 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 18:17:21 -0400
commit5eee5f4a3b11c467c853f8397c7f679e5d5acc7a (patch)
treee7e2de799c3ac84bba0d9d4e6df73e9fe1ca5fcb /src/source.sml
parenta2f45884de59da6607cdb38080b956193e2e883f (diff)
include
Diffstat (limited to 'src/source.sml')
-rw-r--r--src/source.sml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/source.sml b/src/source.sml
index 6397bd71..266e8629 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -67,6 +67,7 @@ datatype sgn_item' =
| SgiCon of string * kind option * con
| SgiVal of string * con
| SgiStr of string * sgn
+ | SgiInclude of sgn
and sgn' =
SgnConst of sgn_item list