Browse Source

Change Ur/Web default display_name

Adam Chlipala 10 years ago
parent
commit
660422a4d2
1 changed files with 1 additions and 0 deletions
  1. 1 0
      frameworks/Ur/urweb/benchmark_config

+ 1 - 0
frameworks/Ur/urweb/benchmark_config

@@ -2,6 +2,7 @@
   "framework": "urweb",
   "tests": [{
     "default": {
+      "display_name": "urweb",
       "setup_file": "setup",
       "json_url": "/json",
       "plaintext_url": "/plaintext",