123456789101112131415161718 |
- <?php
- /* For licensing terms, see /license.txt */
- /**
- * Temporary fix to set user.user_id to the same as user.id
- */
- if (PHP_SAPI != 'cli') {
- die('This script can only be executed from the command line');
- }
- require __DIR__.'/../../main/inc/conf/configuration.php';
- $dbh = mysql_connect(
- $_configuration['db_host'],
- $_configuration['db_user'],
- $_configuration['db_password']
- );
- $db = mysql_select_db($_configuration['main_database']);
- $sql = "UPDATE user SET user_id = id";
- mysql_query($sql);
|