diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 11:20:52 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 11:41:21 +0200 |
| commit | 88d5621e0d70482e5869e9b422ff30b14f58691a (patch) | |
| tree | a75a129b4de6f37b58bc1f89a79f1991d06e3dd0 /plugins | |
| parent | bf5763c6d871d70a4629f378d138ffbf26b765d6 (diff) | |
g_tactics : remove opt_bindings (2-line dead code)
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions