re-add accidentally deleted line from commit bc4209681c

This commit is contained in:
Thomas Gubler
2014-11-28 14:18:30 +01:00
parent bc4209681c
commit cefccc0037
+2
View File
@@ -65,3 +65,5 @@ private:
}; };
extern bool task_should_exit; extern bool task_should_exit;
} // namespace px4