diff options
Diffstat (limited to 'src/www/gfse/editor.js')
| -rw-r--r-- | src/www/gfse/editor.js | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js index e59afdefb..703886ab5 100644 --- a/src/www/gfse/editor.js +++ b/src/www/gfse/editor.js @@ -1277,12 +1277,13 @@ function draw_opers(g,ci) { } function delete_lin(g,ci,fun) { - var i; var c=g.concretes[ci]; - for(i=0;i<c.lins.length && c.lins[i].fun!=fun;i++); - if(i<c.lins.length) c.lins=delete_ix(c.lins,i); - timestamp(c); - reload_grammar(g); + var i=lin_index(c,fun); + if(i!=null) { + c.lins=delete_ix(c.lins,i); + timestamp(c); + reload_grammar(g); + } } /* -------------------------------------------------------------------------- */ |