aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-14 14:07:56 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-14 14:07:56 -0500
commitf7db36644bdbde7b0ed48daffeb760bd5418bd2e (patch)
treed009d124587d5ea580081e4d2fccfb6ac9c21d69 /src/sources
parentf75d359eeaaca5884d515380b735826532fad15c (diff)
Start of RPCification
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sources b/src/sources
index 05b1cc54..f5574365 100644
--- a/src/sources
+++ b/src/sources
@@ -108,6 +108,9 @@ especialize.sml
defunc.sig
defunc.sml
+rpcify.sig
+rpcify.sml
+
tag.sig
tag.sml