diff options
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index 5995a9600..94cba5e0c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -95,6 +95,10 @@ let add_anonymous_entry node = add_entry sp node; sp +let add_absolutely_named_lead sp obj = + cache_object (sp,obj); + add_entry sp (Leaf obj) + let add_leaf id kind obj = let sp = make_path id kind in cache_object (sp,obj); |