diff options
| author | Sébastien Dailly <sebastien@chimrod.com> | 2021-03-21 20:24:15 +0100 |
|---|---|---|
| committer | Sébastien Dailly <sebastien@dailly.me> | 2022-02-07 16:43:33 +0100 |
| commit | 210a4d94836d07bb71cad46b3e670c1977cfe833 (patch) | |
| tree | 406de4546a3530416a5672a16561fbd2b9bd627e /editor/plugins.ml | |
| parent | ccd68208146e87b9f185f543aadccc1110e72642 (diff) | |
Updated PM examples
Diffstat (limited to 'editor/plugins.ml')
| -rwxr-xr-x | editor/plugins.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/editor/plugins.ml b/editor/plugins.ml index 8dd960a..69319c4 100755 --- a/editor/plugins.ml +++ b/editor/plugins.ml @@ -116,6 +116,7 @@ let default pm schema = let props = PM.Example.options schema in props##.menuBar := Js.some Js._true; props##.floatingMenu := Js.some Js._true; + props##.menuContent := (Footnotes.build_menu pm schema)##.fullMenu; let setup = PM.Example.example_setup pm props in let keymaps = |