Index: soft/giet_vm/boot/boot_init.c
===================================================================
--- soft/giet_vm/boot/boot_init.c	(revision 235)
+++ soft/giet_vm/boot/boot_init.c	(revision 236)
@@ -590,7 +590,25 @@
     }
 
-    // set PTE2 after checking double mapping error
+    // set PTE2 
     pt_flags = (unsigned int *) (ptba + 8 * ix2);
     pt_ppn = (unsigned int *) (ptba + 8 * ix2 + 4);
+
+    *pt_flags = flags;
+    *pt_ppn = ppn;
+
+/*
+if ( vpn == 0x00000300)
+{
+boot_puts("vpn       = ");
+boot_putx( vpn );
+boot_puts("\n");
+boot_puts("pt_flags  = ");
+boot_putx( (unsigned int)pt_flags );
+boot_puts("\n");
+boot_puts("*pt_flags = ");
+boot_putx( *pt_flags );
+boot_puts("\n");
+boot_exit();
+}
 
     if ((*pt_flags & PTE_V) != 0) {  // page already mapped
@@ -602,8 +620,5 @@
         boot_exit();
     }
-    // set PTE2
-    *pt_flags = flags;
-    *pt_ppn = ppn;
-
+*/
 }                // end boot_add_pte()
 
@@ -1007,5 +1022,5 @@
         }
     }
-} // end boot_pseg_init()
+} // end boot_psegs_init()
 
 
@@ -1038,6 +1053,5 @@
 
 #if BOOT_DEBUG_PT
-        boot_puts
-            ("\n[BOOT DEBUG] ****** mapping private vsegs in vspace ");
+        boot_puts("\n[BOOT DEBUG] ****** mapping private vsegs in vspace ");
         boot_puts(vspace[vspace_id].name);
         boot_puts(" ******\n");
@@ -1716,52 +1730,29 @@
             boot_puts(") allocated to processor ");
             boot_putd(gpid);
-            boot_puts("  - ctx[LTID]   = ");
+            boot_puts("\n  - ctx[LTID]   = ");
             boot_putd(ltid);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[SR]     = ");
+            boot_puts("\n  - ctx[SR]     = ");
             boot_putx(ctx_sr);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[SR]     = ");
+            boot_puts("\n  - ctx[SR]     = ");
             boot_putx(ctx_sp);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[RA]     = ");
+            boot_puts("\n  - ctx[RA]     = ");
             boot_putx(ctx_ra);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[EPC]    = ");
+            boot_puts("\n  - ctx[EPC]    = ");
             boot_putx(ctx_epc);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[PTPR]   = ");
+            boot_puts("\n  - ctx[PTPR]   = ");
             boot_putx(ctx_ptpr);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[TTY]    = ");
+            boot_puts("\n  - ctx[TTY]    = ");
             boot_putd(ctx_tty);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[NIC]    = ");
+            boot_puts("\n  - ctx[NIC]    = ");
             boot_putd(ctx_nic);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[TIMER]  = ");
+            boot_puts("\n  - ctx[TIMER]  = ");
             boot_putd(ctx_timer);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[DMA]    = ");
+            boot_puts("\n  - ctx[DMA]    = ");
             boot_putd(ctx_dma);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[PTAB]   = ");
+            boot_puts("\n  - ctx[PTAB]   = ");
             boot_putx(ctx_ptab);
-            boot_puts("\n");
-
-            boot_puts("  - ctx[VSID]   = ");
+            boot_puts("\n  - ctx[VSID]   = ");
             boot_putd(vspace_id);
             boot_puts("\n");
-
 #endif
 
@@ -1784,4 +1775,5 @@
 /////////////////////////////////////////////////////////////////////
 void boot_init() {
+
     // mapping_info checking
     boot_check_mapping();
