diff options
author | Juan Linietsky <reduzio@gmail.com> | 2016-05-21 23:20:49 -0300 |
---|---|---|
committer | Juan Linietsky <reduzio@gmail.com> | 2016-05-21 23:20:49 -0300 |
commit | 81fd4598c1e436c9dfe7951b1f829ff68045103b (patch) | |
tree | 604a356ffdc305d0b1abad17e7bd0f1d246cff62 | |
parent | 62b568ebbf3837d4d0cae90f55b5ca834fe0dd9a (diff) |
fixed compilation bug
-rw-r--r-- | tools/editor/editor_profiler.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/editor/editor_profiler.h b/tools/editor/editor_profiler.h index aca3220717..f5cea118ce 100644 --- a/tools/editor/editor_profiler.h +++ b/tools/editor/editor_profiler.h @@ -94,6 +94,8 @@ private: //int cursor_metric; int hover_metric; + float graph_height; + bool seeking; Timer *frame_delay; |