src/drivers/mic/driver_mic_source.c: remove wrong code

src/drivers/mic/driver_mic_source.c

@@ -548,11 +548,6 @@ void *_starpu_mic_src_worker(void *arg)
 
 	_starpu_src_common_worker(worker_set, baseworkerid, mic_nodes[devid]);
 
-	_STARPU_TRACE_WORKER_DEINIT_START;
-
-	worker->worker_is_initialized = 0;
-	_STARPU_TRACE_WORKER_DEINIT_END(_STARPU_FUT_CUDA_KEY);
-
 	return NULL;
 
 }