diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/merge.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 26f49f6d49..ccc37046f9 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -1023,9 +1023,3 @@ let relprinctype_to_funprinctype relprinctype nfuns = url = "citeseer.ist.psu.edu/bundy93rippling.html" } *) -(* -*** Local Variables: *** -*** compile-command: "make -C ../.. plugins/funind/merge.cmo" *** -*** indent-tabs-mode: nil *** -*** End: *** -*) |