diff options
-rw-r--r-- | captain/web.f90 | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/captain/web.f90 b/captain/web.f90 index eedb254..55d8ad2 100644 --- a/captain/web.f90 +++ b/captain/web.f90 @@ -747,6 +747,19 @@ contains end function generate_one_player_html + function file_or_compressed_file_exists(filename) result(file_exists) + implicit none + + character(len=*), intent(in)::filename + logical::file_exists + + inquire(file=filename, exist=file_exists) + if(.not. file_exists) then + inquire(file=trim(filename)//".gz", exist=file_exists) + end if + + end function file_or_compressed_file_exists + function generate_one_job_html(req) result(res) use captain_db use config @@ -810,7 +823,8 @@ contains status = get_status_utf8(tasks(i)%status) task_results_filename => get_task_result_static_filename(one_job%id, i, no_path=.true.) local_task_results_filename => get_task_result_static_filename(one_job%id, i, no_path=.false.) - inquire(file=local_task_results_filename, exist=file_exists) + + file_exists = file_or_compressed_file_exists(local_task_results_filename) write(task_text, '(I8)') i |