diff --git a/docs/src/user.tex b/docs/src/user.tex
index 3b9d3773ca..a50300327c 100644
--- a/docs/src/user.tex
+++ b/docs/src/user.tex
@@ -1770,7 +1770,7 @@ editing \path{grub.conf}.
  possibilities are `bvt' (default), `atropos' and `rrobin'. 
  For more information see Section~\ref{s:sched}. 
 
-\item [pci\_dom0\_hide=(xx.xx.x)(yy.yy.y)\ldots ] 
+\item [physdev\_dom0\_hide=(xx:xx.x)(yy:yy.y)\ldots ]
 Hide selected PCI devices from domain 0 (for instance, to stop it
 taking ownership of them so that they can be driven by another
 domain).  Device IDs should be given in hex format.  Bridge devices do