diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/www/gfse/editor.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/www/gfse/editor.js b/src/www/gfse/editor.js index 56520018d..381cf33a7 100644 --- a/src/www/gfse/editor.js +++ b/src/www/gfse/editor.js @@ -1297,7 +1297,7 @@ function draw_lins(g,ci) { var fty=function_type(g,f.fun) var linty=lintype(g,conc,igs,dc,fty) if(fty) - fn.title=f.fun+": "+show_type(fty) + fn.title="fun "+f.fun+": "+show_type(fty) +"\nlin "+f.fun+": "+show_lintype(linty) var l=[fn] for(var i=0; i<f.args.length;i++) { |