chore: add_del_cmd_form ctrl_enter submit

web/app/controllers/list_manage.php

@@ -282,7 +282,7 @@ if ($cur_tab == 'profile') {
 							echo HTML::tag_end('tr');
 						},
 						[
-							'page_len' => 50,
+							'echo_full' => true,
 							'div_classes' => ['table-responsive'],
 							'table_classes' => ['table', 'align-middle'],
 							'print_after_table' => function () use ($n_problems) {

web/app/controllers/problem_permissions_manage.php

@@ -52,7 +52,6 @@ $managers_form = newAddDelCmdForm(
 		'help' => '命令格式：命令一行一个，<code>+mike</code> 表示把 <code>mike</code> 加入管理者，<code>-mike</code> 表示把 <code>mike</code> 从管理者中移除。',
 	]
 );
-
 $managers_form->runAtServer();
 
 if (isSuperUser(Auth::user())) {

web/app/libs/uoj-form-lib.php

@@ -3,6 +3,7 @@ define('SCRIPT_REFRESH_AS_GET', '<script>;window.location = window.location.orig
 
 function newAddDelCmdForm($form_name, $validate, $handle, $final = null, $cfg = []) {
 	$form = new UOJForm($form_name);
+	$form->config['ctrl_enter_submit'] = true;
 	$form->addTextArea("{$form_name}_cmds", [
 		'label' => '命令',
 		'input_class' => 'form-control font-monospace',