gmp_random was deleted as of PHP 8.0.0.

already documented in appendices/migration80/incompatible.xml.

Author: mumumu

reference/gmp/functions/gmp-random.xml

@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="utf-8"?>
 <!-- $Revision$ -->
-<!-- EN-Revision: c035f0005ac3bfc38d9efed218d763329e0c0fd3 Maintainer: hirokawa Status: ready -->
+<!-- EN-Revision: 7431c7296886d6b8481dfda0284789873e1dbea8 Maintainer: hirokawa Status: ready -->
 <!-- Credits: mumumu -->
 <refentry xmlns="http://docbook.org/ns/docbook" xml:id="function.gmp-random">
  <refnamediv>
@@ -9,7 +9,7 @@
  </refnamediv>
 
  <refsynopsisdiv>
-  &warn.deprecated.function-7-2-0;
+  &warn.deprecated.function-7-2-0.removed-8-0-0;
  </refsynopsisdiv>
 
  <refsect1 role="description">