Make table header more concise

mhauru · mhauru · commit 37f1e9321230 · 2025-03-03T12:31:03.000Z
diff --git a/benchmarks/benchmarks.jl b/benchmarks/benchmarks.jl
@@ -97,7 +97,7 @@ header = [
     "AD Backend",
     "VarInfo Type",
     "Linked",
-    "Evaluation Time / Reference Time",
+    "Eval Time / Ref Time",
     "AD Time / Eval Time",
 ]
 PrettyTables.pretty_table(

Original file line number	Diff line number	Diff line change
`@@ -97,7 +97,7 @@ header = [`
`97`	`97`	`"AD Backend",`
`98`	`98`	`"VarInfo Type",`
`99`	`99`	`"Linked",`
`100`		`- "Evaluation Time / Reference Time",`
	`100`	`+ "Eval Time / Ref Time",`
`101`	`101`	`"AD Time / Eval Time",`
`102`	`102`	`]`
`103`	`103`	`PrettyTables.pretty_table(`