From fb7425c5fe85f471b56b16252997ca31fc0a106f Mon Sep 17 00:00:00 2001
From: Tony Garnock-Jones <tonyg@leastfixedpoint.com>
Date: Mon, 7 Dec 2020 23:44:55 +0100
Subject: [PATCH] Better Javadoc linking

---
 build.xml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/build.xml b/build.xml
index 5054d74..d636b9b 100644
--- a/build.xml
+++ b/build.xml
@@ -26,6 +26,7 @@
   <target name="javadoc">
     <javadoc destdir="doc" access="public">
       <sourcepath path="src/main/java"/>
+      <link href="https://docs.oracle.com/en/java/javase/11/docs/api/"/>
     </javadoc>
   </target>