diff options
Diffstat (limited to 'kern/sched.c')
| -rw-r--r-- | kern/sched.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kern/sched.c b/kern/sched.c index f797409..21b2c90 100644 --- a/kern/sched.c +++ b/kern/sched.c @@ -358,6 +358,7 @@ void destroy_thread(thread_t* t) { free_user_pages(r->paddr, r->size / PAGE_SIZE); } vector_free(&p->regions); + /** PV guests' page tables are managed by pv_pd_t */ if (p->pv == NULL) { destroy_pd(p->cr3); } else { @@ -726,6 +727,7 @@ void kill_current() { free_user_pages(r->paddr, r->size / PAGE_SIZE); } vector_free(&p->regions); + /** PV guests' page tables are managed by pv_pd_t */ if (p->pv == NULL) { destroy_pd(old_cr3); } else { |