|
@@ -36,11 +36,6 @@ const RUNNING_CLASS = 'jp-RunningSessions';
|
|
|
*/
|
|
|
const HEADER_CLASS = 'jp-RunningSessions-header';
|
|
|
|
|
|
-/**
|
|
|
- * The class name added to a running widget header title.
|
|
|
- */
|
|
|
-const TITLE_CLASS = 'jp-RunningSessions-headerTitle';
|
|
|
-
|
|
|
/**
|
|
|
* The class name added to a running widget header refresh button.
|
|
|
*/
|
|
@@ -139,12 +134,7 @@ class RunningSessions extends Widget {
|
|
|
let sessions = document.createElement('div');
|
|
|
sessions.className = `${SECTION_CLASS} ${SESSIONS_CLASS}`;
|
|
|
|
|
|
- let title = document.createElement('span');
|
|
|
- title.textContent = 'Currently Running Jupyter Processes';
|
|
|
- title.className = TITLE_CLASS;
|
|
|
- header.appendChild(title);
|
|
|
-
|
|
|
- let refresh = document.createElement('span');
|
|
|
+ let refresh = document.createElement('button');
|
|
|
refresh.className = REFRESH_CLASS;
|
|
|
header.appendChild(refresh);
|
|
|
|