diff --git a/tools/project_manager/diff.php b/tools/project_manager/diff.php index f7a27a685..db2c60216 100644 --- a/tools/project_manager/diff.php +++ b/tools/project_manager/diff.php @@ -32,19 +32,11 @@ } $project = new Project($projectid); +// validate that the page exists within the project +$project->get_project_page($image); $state = $project->state; $project_title = $project->nameofwork; -if (!$project->pages_table_exists) { - // This shouldn't normally happen -- - // if the page table doesn't exist, a "diff" link shouldn't be shown. - // But a user might have a bookmarked or otherwise saved a 'diff' URL. - echo "
", _("Page details are not available for this project."), "
\n"; - echo "", _("Project ID"), ": $projectid
\n"; - echo "", _("Title"), ": " . html_safe($project_title) . "
\n"; - exit; -} - // -------------------------------------------------------------- // get information about this diff $L_format = $L_round->id == "OCR" ? false : is_formatting_round($L_round);