Initial comit - Clone

2024-03-05 22:01:20 +01:00
commit 385cf8e5aa
727 changed files with 164567 additions and 0 deletions
--- a/plugins/jingoo/dune
+++ b/plugins/jingoo/dune
@@ -0,0 +1,12 @@
+(alias
+ (name plugin)
+ (deps plugin_jingoo.cmxs))
+
+(executable
+ (name plugin_jingoo)
+ (libraries geneweb.gwd_lib)
+ (embed_in_plugin_libraries jingoo)
+ (flags -linkall)
+ (modes
+  (native plugin))
+ (modules plugin_jingoo))
--- a/plugins/jingoo/plugin_jingoo.ml
+++ b/plugins/jingoo/plugin_jingoo.ml