diff options
| author | hallgren <hallgren@chalmers.se> | 2012-09-30 19:53:57 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2012-09-30 19:53:57 +0000 |
| commit | 00490c07dd13c2efeff44fb88c7d8255e8e5a05a (patch) | |
| tree | 76a44c680637270636787d527cbc0b623fe2e806 /src | |
| parent | 5f3e3e8fa2778c111662def0c281189af0c228f4 (diff) | |
gfse: small linearization type display adjustment
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++) { |