message: Tweak description of batch execute
diff: {
  "command": "lean.batchExecute",
  "title": "Lean: Batch Execute File",
  - "description": "Display the goal at the current position."
  + "description": "Execute the current file using Lean"
  }
  ],
  "languages": [
  