aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-02-15 20:52:44 +0100
committerPierre-Marie Pédrot2014-05-12 14:01:10 +0200
commit0f2475ae87a89344a50b323e47765b61e3e3eb59 (patch)
tree4b628d6578463731ddfdd046bf9433b27ee92cbe /kernel/type_errors.ml
parent9f8d5a9bcae4c4ca4d761e7ae0c2fdc99bcb1340 (diff)
Plugin names must be declared in the header of .ml4 file, be they static or
dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions