diff --git a/functions/info.xml b/functions/info.xml
index beac280174..68d12c4043 100644
--- a/functions/info.xml
+++ b/functions/info.xml
@@ -594,8 +594,8 @@ echo $dat["ru_utime.tv_usec"]; # user time used (microseconds)
     <para>
      Not all the available options can be changed using
      <function>ini_set</function>. Below is a table with a list of all
-     option (as of PHP 4.0.5-dev), indicating which ones can be changed/set
-     and at what level.
+     PHP options (as of PHP 4.0.5-dev), indicating which ones can be 
+     changed/set and at what level.
      <table>
       <title>Configuration options</title>
       <tgroup cols="3">