diff options
Diffstat (limited to 'ide/typed_notebook.ml')
| -rw-r--r-- | ide/typed_notebook.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml index bd26bab273..ad122ee2bd 100644 --- a/ide/typed_notebook.ml +++ b/ide/typed_notebook.ml @@ -54,7 +54,9 @@ object(self) method pages = term_list - method current_term = List.nth term_list super#current_page + method current_term = + List.nth term_list super#current_page + end let create build = |