diff options
author | 2018-04-05 18:02:11 +0200 | |
---|---|---|
committer | 2018-04-05 18:02:11 +0200 | |
commit | 1df2f844240e8349ea4fa82519076a514edaaa0c (patch) | |
tree | 8a4dcd5d8706f0f353fcfd92813a0a650d30f895 /ide/wg_RoutedMessageViews.mli | |
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 'ide/wg_RoutedMessageViews.mli')
0 files changed, 0 insertions, 0 deletions