diff options
| author | hallgren <hallgren@chalmers.se> | 2012-08-02 12:54:15 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2012-08-02 12:54:15 +0000 |
| commit | 7f6c248bf1623a3e0ae5b1f4d7885bd4a54edc6e (patch) | |
| tree | 7a657b55297fcb92bf84cf080b6c239e7517de7b /src/example-based/ExampleDemo.hs | |
| parent | 2e968a01fab7089b3b918b3944ba324ff95c337b (diff) | |
translator: keep cloud docs and local docs apart
+ show a cloud icon next to the document name if it is stored in the cloud
+ in addition to the name of the current document, remember if it is stored in
the cloud, so that the right document is loaded next time you open the
translator.
Diffstat (limited to 'src/example-based/ExampleDemo.hs')
0 files changed, 0 insertions, 0 deletions