Resetting Old Media Wiki Passwords in MySQL

I needed to reset a forgotten user password in an older version of Mediawiki that predates the changePassword.php utility. Also, email notifications were disabled.  These are some clarifications of the instructions from http://www.mediawiki.org/wiki/Manual:FAQ#How_do_I_reset_a_password.3F.   Here are the steps:

1. Look at your LocalSettings.php file to remind yourself of the DB name, the DB prefix, user name and password associated with your Mediawiki installation.  Let's say they are mywikidb, mywikiprefix, mywikiuser, and mywikipass, respectively.  
2. Login from the command line to your mysql:   mysql -u mywikiuser -pmywikipass
3. Change to the database at the mysql prompt: USE mywikidb;
4. Verify things: SHOW columns FROM mywikiprefixuser;
5. Verify more things: SELECT user_name, user_id, user_real_name, user_email FROM mywikiprefixuser;
6. Change the password: UPDATE mywikiprefixuser SET user_password = MD5(CONCAT(user_id, '-', MD5('newpass'))) WHERE user_name="someuser";

In step 6, change mywikiprefix to your prefix, newpass to the desired password, and someuser to the appropriate user of your system.  In step 5, you should see the user_name value ("JimboWales"), so this is a useful check.