diff options
| author |  Artyom Shalkhakov <artyom.shalkhakov@gmail.com> | 2019-01-27 16:01:20 +0200 |
|---|---|---|
| committer | Artyom Shalkhakov <artyom.shalkhakov@gmail.com> | 2019-01-27 16:01:20 +0200 |
| commit | 949a2d6767aeec22a029c353b8a12be3665e60ec (patch) | |
| tree | dc9b6846676dde5158450465766f4eb6963ff932 | |
| parent | ff20f86eb6e792b69c2b580444bd9b051aaf7752 (diff) | |
Fix build error.
| -rw-r--r-- | src/sources | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sources b/src/sources index 5c0b2a84..851cdc16 100644 --- a/src/sources +++ b/src/sources @@ -165,6 +165,9 @@ $(SRC)/css.sml $(SRC)/mono.sml +$(SRC)/endpoints.sig +$(SRC)/endpoints.sml + $(SRC)/mono_util.sig $(SRC)/mono_util.sml |