diff options
Diffstat (limited to 'plugins/derive/Derive.v')
| -rw-r--r-- | plugins/derive/Derive.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/Derive.v b/plugins/derive/Derive.v index 0d5a93b0..d1046ae7 100644 --- a/plugins/derive/Derive.v +++ b/plugins/derive/Derive.v @@ -1 +1 @@ -Declare ML Module "derive_plugin".
\ No newline at end of file +Declare ML Module "derive_plugin". |