What does /*!xxxxxx statement */ generated by mysqldump mean?

I was always curious about what these comment enclosed preprocess开发者_如何学JAVAor-like statements that mysqldump generates for me mean. Here's an example:

/*!40000 ALTER TABLE abc DISABLE KEYS */;

The general pattern seems to be

/*![some numeric code] [some statement] */;

Please point to proper documentation if exists. Otherwise explain. :)

http://dev.mysql.com/doc/refman/5.1/en/comments.html

Comments of the form /*! stuff */ are treated as comments by other RDBMSs, but MySQL will read what's inside the comment and execute it as SQL. You can use this to take advantage of MySQL-specific features even using code that might be run against other RDBMSs. For example you could use /*! ENGINE=INNODB */ in a CREATE TABLE query.

The numbers are optional and if you use them then MySQL will ignore them if its version number is less than the number (with dots inserted in the appropriate places).