aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorMaxime Dénès2019-11-01 15:53:30 +0100
committerMaxime Dénès2019-11-01 15:53:30 +0100
commitfdabd4dbd6bfd60ad46fc8c945ed063860498e53 (patch)
tree01edf91f8b536ad4acfbba39e114daa06b40f3f8 /Makefile.common
parentd00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (diff)
parentacdaab2a8c2ccb63df364bb75de8a515b2cef484 (diff)
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common
index 1ad255d156..e392e51153 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -149,6 +149,7 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
SYNTAXCMO:=$(addprefix plugins/syntax/, \
r_syntax_plugin.cmo \
int63_syntax_plugin.cmo \
+ float_syntax_plugin.cmo \
numeral_notation_plugin.cmo \
string_notation_plugin.cmo)
DERIVECMO:=plugins/derive/derive_plugin.cmo