소스 검색

Merge pull request #1364 from achlipala/master

Change Ur/Web default display_name
Brittany Mazza 10 년 전
부모
커밋
8f5d30661e
1개의 변경된 파일1개의 추가작업 그리고 0개의 파일을 삭제
  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",