Skip to content

Commit

Permalink
Disable dynload of plugin-indent
Browse files Browse the repository at this point in the history
  • Loading branch information
Laporte committed Apr 5, 2017
1 parent 148448e commit 1079b8c
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions plugins/ocp-lint-plugin-indent/build.ocp
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,11 @@
(**************************************************************************)

begin library "ocp-lint-plugin-indent"
install_META = true
install_subdir = "ocp-lint-plugins"
(* Uncomment when: *)
(* * ocp-indent'META has field plugin *)
(* * ocp-intent installs its .cmxs *)
(* install_META = true *)
(* install_subdir = "ocp-lint-plugins" *)
files = [
"plugin_indent.ml"
"ocp_indent.ml"
Expand Down

0 comments on commit 1079b8c

Please sign in to comment.