diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-05 18:02:11 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-05 18:02:11 +0200 |
| commit | 1df2f844240e8349ea4fa82519076a514edaaa0c (patch) | |
| tree | 8a4dcd5d8706f0f353fcfd92813a0a650d30f895 /plugins/funind | |
| parent | 332efef9073eadb4907cd4e9ee1ba17bcc16afc6 (diff) | |
Remove unused script.
This is dead code since fd44a40f9d426a7b65f167bc30d320a0f7dd2bbd.
This script was initially introduced in a088d03434417e935df3c75f81a954eadbdfc2b8
and left untouched since then.
Diffstat (limited to 'plugins/funind')
0 files changed, 0 insertions, 0 deletions