From 31ffacb2d718c0ee55cee036b6493ae49448be22 Mon Sep 17 00:00:00 2001
From: Benjamin Moosherr <benjamin.moosherr@uni-ulm.de>
Date: Thu, 12 Jun 2025 23:13:16 +0200
Subject: [PATCH] fix: Manually move generated javadoc to docs/javadoc

The dependency update of the maven-javadoc-plugin in
afd65e1d9079b9d1ea698c9ffb9e3322914e10c5 removed the possibility to
define an alternative output directory for the generated javadoc which
resulted in a warning that I missed until now. This regression was
intentional and is declared as won't fix by upstream. See
https://github.com/apache/maven-javadoc-plugin/issues/1194
---
 default.nix | 1 +
 pom.xml     | 2 --
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/default.nix b/default.nix
index b1988548e..9503cc2f2 100644
--- a/default.nix
+++ b/default.nix
@@ -122,6 +122,7 @@ pkgs.stdenvNoCC.mkDerivation rec {
       if buildGitHubPages
       then ''
         mvn javadoc:javadoc
+        mv target/reports/apidocs docs/javadoc
         JEKYLL_ENV=production PAGES_REPO_NWO=VariantSync/DiffDetective JEKYLL_BUILD_REVISION= PAGES_DISABLE_NETWORK=1 github-pages build
         rm -rf _site/target
       ''
diff --git a/pom.xml b/pom.xml
index 7a03c05fd..667e8d292 100644
--- a/pom.xml
+++ b/pom.xml
@@ -46,8 +46,6 @@
                 <artifactId>maven-javadoc-plugin</artifactId>
                 <version>3.11.2</version>
                 <configuration>
-                    <reportOutputDirectory>docs</reportOutputDirectory>
-                    <destDir>javadoc</destDir>
                     <show>private</show>
                     <quiet>true</quiet>
                 </configuration>