diff --git a/Documentation/NuttxUserGuide.html b/Documentation/NuttxUserGuide.html
index 8eecc9052b2..26079b5752e 100644
--- a/Documentation/NuttxUserGuide.html
+++ b/Documentation/NuttxUserGuide.html
@@ -9743,25 +9743,25 @@ notify a task when a message is available on a queue.
 <p>
   Where argc is the number of uint32_t type arguments that follow.
 </p>
-  The arguments are passed as uint32_t values.
-  For systems where the sizeof(pointer) &lt; sizeof(uint32_t), the
-  following union defines the alignment of the pointer within the
-  uint32_t.  For example, the SDCC MCS51 general pointer is
-  24-bits, but uint32_t is 32-bits (of course).
-</p>
-<pre>
-    union wdparm_u
-    {
-      void   *pvarg;
-      uint32_t *dwarg;
-    };
-    typedef union wdparm_u wdparm_t;
-</pre>
 <p>
-  For most 32-bit systems, pointers and uint32_t are the same size
-  For systems where sizeof(pointer) > sizeof(uint32_t), we will
-  have to do some redesign.
+  The arguments are passed as <code>wdparm_t</code> values.  For systems where the <code>sizeof(pointer) &lt; sizeof(uint32_t)</code>, the following union defines the alignment of the pointer within the <code>uint32_t</code>.  For example, the SDCC MCS51 general pointer is 24-bits, but <code>uint32_t</code> is 32-bits (of course).
 </p>
+   We always have <code>sizeof(pointer) <= sizeof(uintptr_t)</code> by definitions.
+</p>
+<ul><pre>
+union wdparm_u
+{
+  FAR void     *pvarg; /* The size one generic point */
+  uint32_t      dwarg; /* Big enough for a 32-bit value in any case */
+  uintptr_t     uiarg; /* sizeof(uintptr_t) >= sizeof(pointer) */
+};
+
+#if UINTPTR_MAX >= UINT32_MAX
+typedef uintptr_t wdparm_t;
+#else
+typedef uint32_t  wdpartm_t;
+#endif
+</pre></ul>
 
 <table width ="100%">
   <tr bgcolor="#e4e4e4">