From febc5677793217866297d9012b67d28181c7974c Mon Sep 17 00:00:00 2001
From: Dennis Diefenbach <dennis.diefenbach@univ-st-etienne.fr>
Date: Tue, 6 Dec 2022 00:12:06 +0100
Subject: [PATCH] Fix bug with java doc

---
 .../src/main/java/org/rdfhdt/hdt/options/HideHDTOptions.java    | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hdt-java-core/src/main/java/org/rdfhdt/hdt/options/HideHDTOptions.java b/hdt-java-core/src/main/java/org/rdfhdt/hdt/options/HideHDTOptions.java
index 5257675a..e9b9b46f 100644
--- a/hdt-java-core/src/main/java/org/rdfhdt/hdt/options/HideHDTOptions.java
+++ b/hdt-java-core/src/main/java/org/rdfhdt/hdt/options/HideHDTOptions.java
@@ -16,7 +16,7 @@ public class HideHDTOptions implements HDTOptions {
 
     /**
      * @param spec   wrapped options
-     * @param mapper mapping function (key) -> newKey?
+     * @param mapper mapping function (key) {@literal ->} newKey?
      */
     public HideHDTOptions(HDTOptions spec, Function<String, String> mapper) {
         this.spec = spec;